aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Collapse)AuthorAgeFilesLines
* fixing a potential inconsistency from unsafe_coerceSylvain Boulmé2019-11-142-7/+13
| | | | | Now, unsafe_coerce axioms are clearly consistent (for any interpretation of may-return monads). But, the extraction is still unsafe...
* removing Focus (deprecated)Sylvain Boulmé2019-11-141-2/+2
|
* Un espace en tropCyril SIX2019-10-211-1/+1
|
* eq_condition already existedDavid Monniaux2019-10-161-6/+0
|
* [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-162-16/+2
| | | | | | | | | | | | | | | | | | | | | | Conflicts: .gitignore backend/Lineartyping.v common/Values.v configure cparser/Machine.ml cparser/Machine.mli driver/Configuration.ml driver/Frontend.ml runtime/Makefile test/c/Makefile test/c/aes.c test/compression/Makefile test/regression/Makefile test/regression/extasm.c test/regression/floats-basics.c test/regression/floats.c Note : test/regression should be checked, didn't test it yet
* Few minor other changes in proofCyril SIX2019-10-151-3/+3
|
* More elaborate comments + rewriting for easier to understand Asmblockgenproof.vCyril SIX2019-10-151-145/+89
|
* Converting mppa_k1c/*.v files to Unix formatCyril SIX2019-10-112-754/+754
|
* Fixing fp_is_parent too weak (#165)Cyril SIX2019-10-112-1798/+1811
|
* Merge branch 'mppa-duplicate-rtl' into mppa-workCyril SIX2019-10-081-0/+6
|\
| * IcondCyril SIX2019-10-071-0/+6
| |
* | Asmblockgenproof : cur rewritingCyril SIX2019-10-011-11/+11
| |
* | Tiny cleanCyril SIX2019-10-011-1/+0
| |
* | Asmblockgenproof renaming fpok --> epCyril SIX2019-10-011-11/+11
|/
* (#161) - Fixing vararg bugCyril SIX2019-09-241-2/+2
|
* __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
|
* 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
|
generated by cgit (git 2.34.1) at 2024-07-06 15:25:43 +0000