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
*
Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...
David Monniaux
2020-02-08
12
-54
/
+84
|
\
|
*
Added base address if needed.
Bernhard Schommer
2020-02-06
3
-33
/
+53
|
*
Compatibility with OCaml 4.10 (#214)
Xavier Leroy
2020-02-06
3
-7
/
+7
|
*
Revised menhirLib autoconfiguration (#331)
Xavier Leroy
2020-02-05
3
-5
/
+9
|
*
Support Coq 8.11.0 (#212)
Xavier Leroy
2020-02-05
4
-2
/
+8
|
*
Incorrect computation of extra stack size for vararg calls in RISC-V (#213)
Bernhard Schommer
2020-02-05
1
-2
/
+2
|
*
Reduce the checking time for the "decidable_equality_from" tactic
xavier.leroy
2020-01-30
1
-4
/
+5
*
|
stubs to keep compiling on architectures not K1c
David Monniaux
2020-02-07
5
-0
/
+15
*
|
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
*
|
|
accessors for records are now not extracted it seems
David Monniaux
2020-02-06
1
-3
/
+3
|
/
/
*
|
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
[next]