aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Collapse)AuthorAgeFilesLines
* Removing unused .all, .any, .nall and .none conditionsCyril SIX2019-09-052-17/+0
|
* compatibility with OCaml 4.08David Monniaux2019-09-032-4/+3
|
* Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-workCyril SIX2019-09-0318-39/+724
|\ | | | | | | | | | | | | Conflicts: configure mppa_k1c/Archi.v mppa_k1c/Asmexpand.ml
| * fma with first negated operandDavid Monniaux2019-08-302-6/+16
| |
| * fmaDavid Monniaux2019-08-3013-15/+154
| |
| * début du fmaDavid Monniaux2019-08-304-7/+179
| |
| * use finvwDavid Monniaux2019-08-303-4/+45
| |
| * add finvw ; not yet generatedDavid Monniaux2019-08-3011-6/+55
| |
| * fabsfDavid Monniaux2019-08-293-1/+10
| |
| * fmin/fmax/fminf/fmaxf non bien testésDavid Monniaux2019-08-2911-11/+93
| |
| * begin implementing minf/maxfDavid Monniaux2019-08-295-11/+128
| |
| * various fixesDavid Monniaux2019-07-194-5/+22
| |
| * helpers broke compilationDavid Monniaux2019-07-193-12/+60
| |
* | Englishification of commentsCyril SIX2019-09-032-11/+6
| |
* | Merge branch 'mppa-work' of ↵David Monniaux2019-08-3118-615/+292
|\ \ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | Rajout de clzd dans les testsCyril SIX2019-08-301-3/+2
| | |
| * | Added more testsCyril SIX2019-08-301-2/+2
| | |
| * | (#157) Removed AFADDD and AFADDW from the builtinsCyril SIX2019-08-304-8/+8
| | |
| * | (#156) - Un peu de cleaning et de docCyril SIX2019-07-3010-497/+53
| | |
| * | (#139) - Quelques renommagesCyril SIX2019-07-304-12/+12
| | |
| * | (#139) - Predicate is_concatCyril SIX2019-07-302-8/+9
| | |
| * | (#139) - Mise à jour du code Coq, oracleCyril SIX2019-07-253-12/+59
| | |
| * | (#145) Fix <bad addressing> on RTL dumpsCyril SIX2019-07-241-1/+2
| | |
| * | (#144) Fixing <bad operator> on RTL dumpsCyril SIX2019-07-242-33/+50
| | |
| * | (#137) Possible fixCyril SIX2019-07-231-1/+4
| | |
| * | (#137) [BROKEN] - Finer latencies for the oracle. Some debugging to doCyril SIX2019-07-221-40/+93
| |/
* / some more proofs on integers, preparing for absolute value instructionDavid Monniaux2019-08-311-0/+18
|/
* Removing a hidden FIXME that hopefully didn't have any impact..Cyril SIX2019-07-181-7/+0
|
* (#137) Removed the useless strings in PostpassSchedulingOracleCyril SIX2019-07-181-337/+254
|
* Typo in PrevsubxwCyril SIX2019-07-181-1/+1
|
* (#107) Rename "forward_simu" into "bisimu"Cyril SIX2019-07-171-27/+27
|
* Replaced the solution -> bundles part by an algorithm hopefully linearCyril SIX2019-07-091-54/+39
|
* Merge branch 'mppa-work' of ↵David Monniaux2019-06-242-21/+19
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * maj forward_simu_par_wio_bblock_aux en forward_simu_par_wioSylvain Boulmé2019-06-232-21/+19
| | | | | | | | avec une legere simplification (comme dans le papier)
* | op printing (still incomplete)David Monniaux2019-06-241-1/+12
| |
* | pretty-printing for extra operations (unfinished)David Monniaux2019-06-241-1/+38
|/
* fix makespan computationDavid Monniaux2019-06-221-1/+3
|
* schedule from endDavid Monniaux2019-06-221-17/+18
|
* -frevlistDavid Monniaux2019-06-212-8/+35
|
* pretty print statisticsDavid Monniaux2019-06-191-36/+33
|
* Reverting the unwanted time measurement from the other branchCyril SIX2019-06-181-14/+1
|
* [NOT TESTED] Compiles and should work ?Cyril SIX2019-06-181-11/+17
|
* [BROKEN] still broken, just fixing a logical detailCyril SIX2019-06-171-1/+1
|
* [BROKEN] Fixed the dependency oracle, does not compileCyril SIX2019-06-171-8/+42
| | | | I was removing too many dependencies
* [NOT TESTED] ça compileCyril SIX2019-06-171-7/+7
|
* [BROKEN] Replaced the accesses lists by Maps, does not compileCyril SIX2019-06-141-8/+58
|
* Removing the Admitted warning when running "make check-admitted"Cyril SIX2019-06-121-1/+1
|
* abstract_bb: few improvements while writing the paperSylvain Boulmé2019-06-086-251/+294
|
* Merge branch 'mppa-work' into mppa-abstractbb-devSylvain Boulmé2019-06-0818-1065/+1539
|\
| * Fix for #134 Pjumptable not recognizedCyril SIX2019-06-051-1/+1
| |
generated by cgit (git 2.34.1) at 2024-07-04 01:43:07 +0000