index
:
compcert-kvx
CPP22_if_lifting
CPP22_main
master
patched_for_velus
riscV-cmov
ssa
vericert
vericert-kvx
Unnamed repository; edit this file 'description' to name the repository.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
Files
Lines
...
|
|
*
|
|
Added option -ftracelinearize which linearizes based on ifnot branches
Cyril SIX
2020-02-12
4
-4
/
+59
|
|
*
|
|
Moving some arch specific theorems from PSproof to Asmblockprops
Cyril SIX
2020-02-11
2
-219
/
+218
|
|
*
|
|
Moving Asmblockgenproof0 to mppa_k1c/lib/
Cyril SIX
2020-02-10
1
-0
/
+0
|
|
*
|
|
Removing from Asmblockgenproof0 architecture specific definitions
Cyril SIX
2020-02-10
9
-130
/
+153
|
|
*
|
|
Moved some theorems
Cyril SIX
2020-02-10
4
-113
/
+101
|
|
*
|
|
bringing back the ppc64 runtime
David Monniaux
2020-02-09
5
-0
/
+440
|
|
*
|
|
Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-merge
David Monniaux
2020-02-08
17
-0
/
+1430
|
|
|
\
\
\
|
|
|
*
|
|
why did we remove the ppc runtime ?!
David Monniaux
2020-02-08
17
-0
/
+1430
|
|
*
|
|
|
Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...
David Monniaux
2020-02-08
12
-54
/
+84
|
|
|
\
\
\
\
|
|
|
|
/
/
/
|
|
|
/
|
|
|
|
|
*
|
|
|
stubs to keep compiling on architectures not K1c
David Monniaux
2020-02-07
5
-0
/
+15
|
*
|
|
|
|
Merge branch 'mppa-work' into mppa-cse2
Cyril SIX
2020-02-06
4
-67
/
+87
|
|
\
|
|
|
|
|
|
*
|
|
|
Merge branch 'mppa-fixing-bundling' into mppa-work
Cyril SIX
2020-02-06
4
-67
/
+87
|
|
|
\
\
\
\
|
|
|
*
|
|
|
Fixing maddw and maddd resource tables
Cyril SIX
2020-02-06
1
-2
/
+19
|
|
|
*
|
|
|
Using Ocaml type instead of string to identify resources
Cyril SIX
2020-02-06
1
-35
/
+36
|
|
|
*
|
|
|
Fixed reservation tables
Cyril SIX
2020-02-06
1
-44
/
+46
|
|
|
*
|
|
|
Breaking the prologue to satisfy resource constraints
Cyril SIX
2020-02-06
1
-1
/
+1
|
|
|
*
|
|
|
Fixed using ccomp assembly preprocessor
Cyril SIX
2020-02-06
1
-3
/
+3
|
|
|
*
|
|
|
Using k1-elf-as instead of k1-cos-gcc for assembling
Cyril SIX
2020-02-03
1
-2
/
+2
|
*
|
|
|
|
|
Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2
David Monniaux
2020-02-06
1
-3
/
+3
|
|
\
|
|
|
|
|
|
|
*
|
|
|
|
accessors for records are now not extracted it seems
David Monniaux
2020-02-06
1
-3
/
+3
|
|
|
/
/
/
/
|
*
|
|
|
|
Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2
David Monniaux
2020-02-06
16
-66
/
+832
|
|
\
|
|
|
|
|
|
*
|
|
|
Added flag to desactivate condition inversion
Cyril SIX
2020-02-03
3
-1
/
+6
|
|
*
|
|
|
Adding threshold to duplicate instructions
Cyril SIX
2020-01-31
1
-6
/
+12
|
|
*
|
|
|
Merge remote-tracking branch 'origin/mppa-work' into mppa-duplicate-oracle
Cyril SIX
2020-01-27
7
-42
/
+187
|
|
|
\
\
\
\
|
|
|
*
|
|
|
Updated scripts to run the tests on test/mppa
Cyril SIX
2020-01-27
5
-7
/
+19
|
|
|
*
|
|
|
Hardware runs for test/mppa/interop
Cyril SIX
2020-01-27
1
-24
/
+113
|
|
|
*
|
|
|
New directive hardtest and hardcheck to run on hardware test/mppa/instr
Cyril SIX
2020-01-27
1
-11
/
+55
|
|
*
|
|
|
|
Tail duplication optimization defaulting to off
Cyril SIX
2020-01-27
2
-2
/
+1
|
|
*
|
|
|
|
Added a flag to desactivate tail duplication
Cyril SIX
2020-01-27
5
-6
/
+17
|
|
*
|
|
|
|
Added debug message when inverting ifso ifnot
Cyril SIX
2020-01-24
1
-1
/
+3
|
|
*
|
|
|
|
Oracle inverting branches when trace does not go in fallthru
Cyril SIX
2020-01-24
1
-2
/
+21
|
|
*
|
|
|
|
Revert "Modified the hook for the oracle"
Cyril SIX
2020-01-23
3
-12
/
+8
|
|
*
|
|
|
|
Verificator finished for handling reversed Icond
Cyril SIX
2020-01-23
2
-11
/
+18
|
|
*
|
|
|
|
Added clause in match_inst to allow Icond reversal
Cyril SIX
2020-01-23
1
-4
/
+13
|
|
*
|
|
|
|
Modified the hook for the oracle
Cyril SIX
2020-01-23
3
-8
/
+12
|
|
*
|
|
|
|
Fixing bug caused by get_predecessors returning duplicates
Cyril SIX
2020-01-23
1
-5
/
+8
|
|
*
|
|
|
|
Printing traces right before duplicating
Cyril SIX
2020-01-23
1
-5
/
+2
|
|
*
|
|
|
|
Fixing bug (used physical instead of structural inequality)
Cyril SIX
2020-01-22
1
-1
/
+2
|
|
*
|
|
|
|
Merge branch 'mppa-work' into mppa-duplicate-oracle
Cyril SIX
2020-01-22
26
-68
/
+1905
|
|
|
\
|
|
|
|
|
|
*
|
|
|
|
Fixing is_empty function
Cyril SIX
2020-01-22
1
-3
/
+3
|
|
*
|
|
|
|
Branch duplication implementation
Cyril SIX
2020-01-22
1
-12
/
+94
|
|
*
|
|
|
|
Set up the groundbase for doing the duplication
Cyril SIX
2020-01-17
1
-4
/
+14
|
|
*
|
|
|
|
Removed unnecessary .mli file (provoked compilation problems)
Cyril SIX
2020-01-17
1
-12
/
+0
|
|
*
|
|
|
|
Adding more debug elements
Cyril SIX
2020-01-15
1
-1
/
+9
|
|
*
|
|
|
|
Typo in printf
Cyril SIX
2020-01-13
1
-1
/
+1
|
|
*
|
|
|
|
Opcode heuristic done for K1c
Cyril SIX
2019-12-16
3
-3
/
+33
|
|
*
|
|
|
|
Stub for opcode heuristic
Cyril SIX
2019-12-16
3
-4
/
+16
|
|
*
|
|
|
|
Fixing loop heuristic for the way CompCert handles loops
Cyril SIX
2019-12-11
1
-11
/
+19
|
|
*
|
|
|
|
Implemented call, return, store and loop heuristics
Cyril SIX
2019-12-11
1
-2
/
+55
|
|
*
|
|
|
|
Function to look ahead unconditionally
Cyril SIX
2019-12-11
1
-0
/
+12
[prev]
[next]