Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Removing from Asmblockgenproof0 architecture specific definitions | Cyril SIX | 2020-02-10 | 8 | -129/+152 |
| | |||||
* | Moved some theorems | Cyril SIX | 2020-02-10 | 4 | -113/+101 |
| | |||||
* | Fixing maddw and maddd resource tables | Cyril SIX | 2020-02-06 | 1 | -2/+19 |
| | |||||
* | Using Ocaml type instead of string to identify resources | Cyril SIX | 2020-02-06 | 1 | -35/+36 |
| | |||||
* | Fixed reservation tables | Cyril SIX | 2020-02-06 | 1 | -44/+46 |
| | |||||
* | Breaking the prologue to satisfy resource constraints | Cyril SIX | 2020-02-06 | 1 | -1/+1 |
| | |||||
* | Merge branch 'mppa-work' into mppa-duplicate-oracle | Cyril SIX | 2020-01-22 | 1 | -0/+132 |
|\ | |||||
| * | Fixing issue with "destruct ... in ..." tactics with Coq 8.8 | Cyril SIX | 2020-01-09 | 1 | -5/+5 |
| | | |||||
| * | swap load and store at disjoint offsets | David Monniaux | 2019-12-16 | 1 | -1/+53 |
| | | |||||
| * | swap stores at disjoint offsets | David Monniaux | 2019-12-16 | 1 | -16/+30 |
| | | |||||
| * | comment out theorem that cannot be proved | David Monniaux | 2019-12-14 | 1 | -29/+33 |
| | | |||||
| * | progress in chunks | David Monniaux | 2019-12-13 | 1 | -45/+9 |
| | | |||||
| * | some subgoal was proved | David Monniaux | 2019-12-12 | 1 | -6/+61 |
| | | |||||
| * | begin overlap proofs | David Monniaux | 2019-12-11 | 1 | -0/+43 |
| | | |||||
* | | Opcode heuristic done for K1c | Cyril SIX | 2019-12-16 | 1 | -2/+30 |
| | | |||||
* | | Stub for opcode heuristic | Cyril SIX | 2019-12-16 | 1 | -0/+4 |
|/ | |||||
* | Converting Asm.v and Asmblockgenproof.v back to Unix format | Cyril SIX | 2019-12-03 | 2 | -2426/+2426 |
| | |||||
* | finish merge | David Monniaux | 2019-12-02 | 2 | -11/+20 |
| | |||||
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load | David Monniaux | 2019-12-02 | 7 | -185/+148 |
|\ | |||||
| * | fixing a potential inconsistency from unsafe_coerce | Sylvain Boulmé | 2019-11-14 | 2 | -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-14 | 1 | -2/+2 |
| | | |||||
| * | Un espace en trop | Cyril SIX | 2019-10-21 | 1 | -1/+1 |
| | | |||||
| * | eq_condition already existed | David Monniaux | 2019-10-16 | 1 | -6/+0 |
| | | |||||
| * | [regression to check!] Merge tag 'v3.6' into mppa-work | Cyril SIX | 2019-10-16 | 2 | -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 proof | Cyril SIX | 2019-10-15 | 1 | -3/+3 |
| | | |||||
| * | More elaborate comments + rewriting for easier to understand Asmblockgenproof.v | Cyril SIX | 2019-10-15 | 1 | -145/+89 |
| | | |||||
| * | Converting mppa_k1c/*.v files to Unix format | Cyril SIX | 2019-10-11 | 2 | -754/+754 |
| | | |||||
| * | Fixing fp_is_parent too weak (#165) | Cyril SIX | 2019-10-11 | 2 | -1798/+1811 |
| | | |||||
| * | Merge branch 'mppa-duplicate-rtl' into mppa-work | Cyril SIX | 2019-10-08 | 1 | -0/+6 |
| |\ | |||||
| | * | Icond | Cyril SIX | 2019-10-07 | 1 | -0/+6 |
| | | | |||||
| * | | Asmblockgenproof : cur rewriting | Cyril SIX | 2019-10-01 | 1 | -11/+11 |
| | | | |||||
| * | | 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 ↵ | David Monniaux | 2019-09-20 | 4 | -18/+5 |
|\ \ | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load | ||||
| * | | 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 ↵ | David Monniaux | 2019-09-20 | 3 | -18/+4 |
| |/ | | | | | | | mppa-work-upstream-merge | ||||
* | | 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 |
| | |