| Commit message (Collapse) | Author | Age | Files | Lines | ||
|---|---|---|---|---|---|---|
| ... | ||||||
| | * | | | | | | | | during merge; still some typing issues | David Monniaux | 2020-02-24 | 2 | -6/+9 | |
| | | | | | | | | | | ||||||
| | * | | | | | | | | fix | David Monniaux | 2020-02-24 | 1 | -4/+5 | |
| | | | | | | | | | | ||||||
| | * | | | | | | | | fix | David Monniaux | 2020-02-24 | 1 | -7/+12 | |
| | |/ / / / / / / | ||||||
| * | | | | | | | | thread local declarations now work | David Monniaux | 2020-02-24 | 1 | -2/+6 | |
| | | | | | | | | | ||||||
| * | | | | | | | | it now works, no more ugly hack to access thread local data | David Monniaux | 2020-02-24 | 1 | -4/+8 | |
| |/ / / / / / / | ||||||
| * | | | | | | | Moving some arch specific theorems from PSproof to Asmblockprops | Cyril SIX | 2020-02-11 | 2 | -219/+218 | |
| | | | | | | | | ||||||
| * | | | | | | | Moving Asmblockgenproof0 to mppa_k1c/lib/ | Cyril SIX | 2020-02-10 | 1 | -0/+0 | |
| | | | | | | | | ||||||
| * | | | | | | | 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 | |
| | | | | | | | | | ||||||
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |