Commit message (Expand) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | | 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 | |
| * | | (#156) - Un peu de cleaning et de doc | Cyril SIX | 2019-07-30 | 10 | -497/+53 | |
| * | | (#139) - Quelques renommages | Cyril SIX | 2019-07-30 | 4 | -12/+12 | |
| * | | (#139) - Predicate is_concat | Cyril SIX | 2019-07-30 | 2 | -8/+9 | |
| * | | (#139) - Mise à jour du code Coq, oracle | Cyril SIX | 2019-07-25 | 3 | -12/+59 | |
| * | | (#145) Fix <bad addressing> on RTL dumps | Cyril SIX | 2019-07-24 | 1 | -1/+2 | |
| * | | (#144) Fixing <bad operator> on RTL dumps | Cyril SIX | 2019-07-24 | 2 | -33/+50 | |
| * | | (#137) Possible fix | Cyril SIX | 2019-07-23 | 1 | -1/+4 | |
| * | | (#137) [BROKEN] - Finer latencies for the oracle. Some debugging to do | Cyril SIX | 2019-07-22 | 1 | -40/+93 | |
| |/ | ||||||
* / | some more proofs on integers, preparing for absolute value instruction | David Monniaux | 2019-08-31 | 1 | -0/+18 | |
|/ | ||||||
* | Removing a hidden FIXME that hopefully didn't have any impact.. | Cyril SIX | 2019-07-18 | 1 | -7/+0 | |
* | (#137) Removed the useless strings in PostpassSchedulingOracle | Cyril SIX | 2019-07-18 | 1 | -337/+254 | |
* | Typo in Prevsubxw | Cyril SIX | 2019-07-18 | 1 | -1/+1 | |
* | (#107) Rename "forward_simu" into "bisimu" | Cyril SIX | 2019-07-17 | 1 | -27/+27 | |
* | Replaced the solution -> bundles part by an algorithm hopefully linear | Cyril SIX | 2019-07-09 | 1 | -54/+39 | |
* | Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe... | David Monniaux | 2019-06-24 | 2 | -21/+19 | |
|\ | ||||||
| * | maj forward_simu_par_wio_bblock_aux en forward_simu_par_wio | Sylvain Boulmé | 2019-06-23 | 2 | -21/+19 | |
* | | op printing (still incomplete) | David Monniaux | 2019-06-24 | 1 | -1/+12 | |
* | | pretty-printing for extra operations (unfinished) | David Monniaux | 2019-06-24 | 1 | -1/+38 | |
|/ | ||||||
* | fix makespan computation | David Monniaux | 2019-06-22 | 1 | -1/+3 |