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
*
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
*
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
|
\
|
|
*
Added description for forward moves
Cyril SIX
2020-01-17
1
-0
/
+1
|
*
Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-work
David Monniaux
2020-01-15
12
-60
/
+419
|
|
\
|
|
*
2-instruction signed division by two on Aarch64
David Monniaux
2020-01-15
3
-24
/
+54
|
|
*
ARM generation of 2-instruction signed division by 2 (as opposed to 3-instruc...
David Monniaux
2020-01-14
2
-3
/
+24
|
|
*
64-bit signed division by two code
David Monniaux
2020-01-14
3
-14
/
+26
|
|
*
shrxl_shrl_3
David Monniaux
2020-01-14
1
-0
/
+52
|
|
*
shrx'1_shr'
David Monniaux
2020-01-14
1
-1
/
+127
|
|
*
rv32: 3-instruction signed divide-by-two sequence (as opposed to 4)
David Monniaux
2020-01-14
3
-14
/
+25
|
|
*
shrx_shr_3
David Monniaux
2020-01-14
1
-0
/
+54
|
|
*
shrx1_shr
David Monniaux
2020-01-14
1
-0
/
+51
|
|
*
Remove __builtin_nop from list of x86 builtins.
Bernhard Schommer
2020-01-03
1
-3
/
+0
|
|
*
Revert "Remove `__builtin_nop` for some architectures. (#208)"
Bernhard Schommer
2020-01-03
14
-3
/
+33
|
|
*
Added error for unknown builtin functions. (#208)
Bernhard Schommer
2019-12-21
1
-1
/
+6
|
|
*
Remove `__builtin_nop` for some architectures. (#208)
Bernhard Schommer
2019-12-21
14
-33
/
+3
|
*
|
Merge remote-tracking branch 'origin/mppa-work' into mppa-forwardmoves
David Monniaux
2020-01-09
2
-6
/
+7
|
|
\
\
|
|
*
|
Fixing issue with <math.h> and fabs
Cyril SIX
2020-01-09
1
-1
/
+2
|
|
*
|
Fixing issue with "destruct ... in ..." tactics with Coq 8.8
Cyril SIX
2020-01-09
1
-5
/
+5
|
*
|
|
FINISHED the forward-moves pass
David Monniaux
2020-01-09
1
-2
/
+6
|
*
|
|
nearly done
David Monniaux
2020-01-09
1
-3
/
+5
|
*
|
|
fix move
David Monniaux
2020-01-09
1
-1
/
+3
|
*
|
|
fix move
David Monniaux
2020-01-09
2
-4
/
+120
|
*
|
|
return is ok
David Monniaux
2020-01-09
1
-14
/
+53
|
*
|
|
proof of return
David Monniaux
2020-01-09
1
-1
/
+59
|
*
|
|
we still have issues with call stacks
David Monniaux
2020-01-09
2
-15
/
+51
|
*
|
|
moving forward with proofs
David Monniaux
2020-01-09
2
-5
/
+20
|
*
|
|
proof for jumptable
David Monniaux
2020-01-09
1
-1
/
+17
|
*
|
|
more proofs
David Monniaux
2020-01-09
1
-1
/
+18
|
*
|
|
fix bug and forward in proofs
David Monniaux
2020-01-09
2
-2
/
+18
|
*
|
|
some more proof
David Monniaux
2020-01-09
1
-3
/
+53
[next]