Commit message (Expand) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
| * | | Tiny clean | Cyril SIX | 2019-10-01 | 1 | -1/+0 | |
| * | | Asmblockgenproof renaming fpok --> ep | Cyril SIX | 2019-10-01 | 1 | -11/+11 | |
| |/ | ||||||
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load | David Monniaux | 2019-09-24 | 1 | -2/+2 | |
|\| | ||||||
| * | (#161) - Fixing vararg bug | Cyril SIX | 2019-09-24 | 1 | -2/+2 | |
* | | is_trapping_op_sound | David Monniaux | 2019-09-23 | 1 | -0/+28 | |
* | | Merge tag 'v3.6_mppa_2019-09-20' of gricad-gitlab.univ-grenoble-alpes.fr:sixc... | David Monniaux | 2019-09-20 | 4 | -18/+5 | |
|\ \ | ||||||
| * | | fix compiling | David Monniaux | 2019-09-20 | 2 | -3/+3 | |
| * | | extraction problems | David Monniaux | 2019-09-20 | 1 | -1/+2 | |
| * | | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstrea... | David Monniaux | 2019-09-20 | 3 | -18/+4 | |
| |/ | ||||||
* | | fix Focus -> { ... } | David Monniaux | 2019-09-20 | 1 | -2/+2 | |
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load | David Monniaux | 2019-09-20 | 6 | -46/+48 | |
|\| | ||||||
| * | __builtin_bswap16, 32 and 64 | Cyril SIX | 2019-09-20 | 2 | -36/+35 | |
| * | Detailing oracle/vérificateur in the timings | Cyril SIX | 2019-09-18 | 2 | -2/+3 | |
| * | Timings for Machblockgen, Asmblockgen and postpass scheduling | Cyril SIX | 2019-09-18 | 2 | -6/+8 | |
| * | Compatibility fix for Coq 8.7.1 | Cyril SIX | 2019-09-13 | 1 | -3/+3 | |
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load | David Monniaux | 2019-09-10 | 2 | -17/+0 | |
|\| | ||||||
| * | Removing unused .all, .any, .nall and .none conditions | Cyril SIX | 2019-09-05 | 2 | -17/+0 | |
* | | asmblockgen works | David Monniaux | 2019-09-08 | 2 | -5/+48 | |
* | | more proofs on notrap2 | David Monniaux | 2019-09-08 | 1 | -9/+53 | |
* | | more proofs on notrap | David Monniaux | 2019-09-08 | 1 | -6/+124 | |
* | | notrap in mppa_k1c ML code | David Monniaux | 2019-09-08 | 3 | -31/+35 | |
* | | a couple "Admitted" and the Coq compiles | David Monniaux | 2019-09-08 | 1 | -12/+18 | |
* | | moving forward with notrap | David Monniaux | 2019-09-08 | 1 | -22/+10 | |
* | | further | David Monniaux | 2019-09-08 | 1 | -3/+20 | |
* | | moving forward on K1C | David Monniaux | 2019-09-07 | 8 | -171/+200 | |
* | | more stuff on non trapping loads | David Monniaux | 2019-09-05 | 1 | -0/+8 | |
* | | more proofs | David Monniaux | 2019-09-05 | 1 | -0/+13 | |
* | | more on notrap | David Monniaux | 2019-09-05 | 5 | -19/+57 | |
* | | forgot this function | David Monniaux | 2019-09-03 | 1 | -2/+0 | |
* | | Value analysis for non trapping loads | David Monniaux | 2019-09-03 | 1 | -0/+20 | |
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load | David Monniaux | 2019-09-03 | 2 | -4/+3 | |
|\| | ||||||
| * | compatibility with OCaml 4.08 | David Monniaux | 2019-09-03 | 2 | -4/+3 | |
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load | David Monniaux | 2019-09-03 | 20 | -50/+730 | |
|\| | ||||||
| * | Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-work | Cyril SIX | 2019-09-03 | 18 | -39/+724 | |
| |\ | ||||||
| | * | fma with first negated operand | David Monniaux | 2019-08-30 | 2 | -6/+16 | |
| | * | fma | David Monniaux | 2019-08-30 | 13 | -15/+154 | |
| | * | début du fma | David Monniaux | 2019-08-30 | 4 | -7/+179 | |
| | * | use finvw | David Monniaux | 2019-08-30 | 3 | -4/+45 | |
| | * | add finvw ; not yet generated | David Monniaux | 2019-08-30 | 11 | -6/+55 | |
| | * | fabsf | David Monniaux | 2019-08-29 | 3 | -1/+10 | |
| | * | fmin/fmax/fminf/fmaxf non bien testés | David Monniaux | 2019-08-29 | 11 | -11/+93 | |
| | * | begin implementing minf/maxf | David Monniaux | 2019-08-29 | 5 | -11/+128 | |
| | * | various fixes | David Monniaux | 2019-07-19 | 4 | -5/+22 | |
| | * | helpers broke compilation | David Monniaux | 2019-07-19 | 3 | -12/+60 | |
| * | | Englishification of comments | Cyril SIX | 2019-09-03 | 2 | -11/+6 | |
* | | | avancement (il faut utiliser Vundef visiblement) | David Monniaux | 2019-09-02 | 1 | -0/+39 | |
|/ / | ||||||
* | | Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe... | David Monniaux | 2019-08-31 | 18 | -615/+292 | |
|\ \ | ||||||
| * | | Rajout de clzd dans les tests | Cyril SIX | 2019-08-30 | 1 | -3/+2 | |
| * | | Added more tests | Cyril SIX | 2019-08-30 | 1 | -2/+2 | |
| * | | (#157) Removed AFADDD and AFADDW from the builtins | Cyril SIX | 2019-08-30 | 4 | -8/+8 |