aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* fix Focus -> { ... }David Monniaux2019-09-201-2/+2
* Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-206-46/+48
|\
| * __builtin_bswap16, 32 and 64Cyril SIX2019-09-202-36/+35
| * Detailing oracle/vérificateur in the timingsCyril SIX2019-09-182-2/+3
| * Timings for Machblockgen, Asmblockgen and postpass schedulingCyril SIX2019-09-182-6/+8
| * Compatibility fix for Coq 8.7.1Cyril SIX2019-09-131-3/+3
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-102-17/+0
|\|
| * Removing unused .all, .any, .nall and .none conditionsCyril SIX2019-09-052-17/+0
* | asmblockgen worksDavid Monniaux2019-09-082-5/+48
* | more proofs on notrap2David Monniaux2019-09-081-9/+53
* | more proofs on notrapDavid Monniaux2019-09-081-6/+124
* | notrap in mppa_k1c ML codeDavid Monniaux2019-09-083-31/+35
* | a couple "Admitted" and the Coq compilesDavid Monniaux2019-09-081-12/+18
* | moving forward with notrapDavid Monniaux2019-09-081-22/+10
* | furtherDavid Monniaux2019-09-081-3/+20
* | moving forward on K1CDavid Monniaux2019-09-078-171/+200
* | more stuff on non trapping loadsDavid Monniaux2019-09-051-0/+8
* | more proofsDavid Monniaux2019-09-051-0/+13
* | more on notrapDavid Monniaux2019-09-055-19/+57
* | forgot this functionDavid Monniaux2019-09-031-2/+0
* | Value analysis for non trapping loadsDavid Monniaux2019-09-031-0/+20
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-032-4/+3
|\|
| * compatibility with OCaml 4.08David Monniaux2019-09-032-4/+3
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-0320-50/+730
|\|
| * Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-workCyril SIX2019-09-0318-39/+724
| |\
| | * 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
* | | avancement (il faut utiliser Vundef visiblement)David Monniaux2019-09-021-0/+39
|/ /
* | Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2019-08-3118-615/+292
|\ \
| * | 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
|/
generated by cgit (git 2.34.1) at 2024-06-12 11:49:41 +0000