Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge branch 'mppa-cse2' of ↵ | David Monniaux | 2020-03-03 | 2176 | -666/+596149 |
|\ | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work | ||||
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2 | David Monniaux | 2020-02-14 | 51 | -456/+2436 |
| |\ | |||||
| | * | Added option -ftracelinearize which linearizes based on ifnot branches | Cyril SIX | 2020-02-12 | 4 | -4/+59 |
| | | | |||||
| | * | 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 | 9 | -130/+153 |
| | | | |||||
| | * | Moved some theorems | Cyril SIX | 2020-02-10 | 4 | -113/+101 |
| | | | |||||
| | * | bringing back the ppc64 runtime | David Monniaux | 2020-02-09 | 5 | -0/+440 |
| | | | |||||
| | * | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-merge | David Monniaux | 2020-02-08 | 17 | -0/+1430 |
| | |\ | |||||
| | | * | why did we remove the ppc runtime ?! | David Monniaux | 2020-02-08 | 17 | -0/+1430 |
| | | | | |||||
| | * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵ | David Monniaux | 2020-02-08 | 12 | -54/+84 |
| | |\ \ | | | |/ | | |/| | | | | | mppa-work-upstream-merge | ||||
| | * | | stubs to keep compiling on architectures not K1c | David Monniaux | 2020-02-07 | 5 | -0/+15 |
| | | | | |||||
| * | | | Merge branch 'mppa-work' into mppa-cse2 | Cyril SIX | 2020-02-06 | 4 | -67/+87 |
| |\| | | |||||
| | * | | Merge branch 'mppa-fixing-bundling' into mppa-work | Cyril SIX | 2020-02-06 | 4 | -67/+87 |
| | |\ \ | |||||
| | | * | | 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 |
| | | | | | |||||
| | | * | | Fixed using ccomp assembly preprocessor | Cyril SIX | 2020-02-06 | 1 | -3/+3 |
| | | | | | |||||
| | | * | | Using k1-elf-as instead of k1-cos-gcc for assembling | Cyril SIX | 2020-02-03 | 1 | -2/+2 |
| | | | | | |||||
| * | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2 | David Monniaux | 2020-02-06 | 1 | -3/+3 |
| |\| | | | |||||
| | * | | | accessors for records are now not extracted it seems | David Monniaux | 2020-02-06 | 1 | -3/+3 |
| | |/ / | |||||
| * | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2 | David Monniaux | 2020-02-06 | 16 | -66/+832 |
| |\| | | |||||
| | * | | Added flag to desactivate condition inversion | Cyril SIX | 2020-02-03 | 3 | -1/+6 |
| | | | | |||||
| | * | | Adding threshold to duplicate instructions | Cyril SIX | 2020-01-31 | 1 | -6/+12 |
| | | | | |||||
| | * | | Merge remote-tracking branch 'origin/mppa-work' into mppa-duplicate-oracle | Cyril SIX | 2020-01-27 | 7 | -42/+187 |
| | |\ \ | |||||
| | | * | | Updated scripts to run the tests on test/mppa | Cyril SIX | 2020-01-27 | 5 | -7/+19 |
| | | | | | |||||
| | | * | | Hardware runs for test/mppa/interop | Cyril SIX | 2020-01-27 | 1 | -24/+113 |
| | | | | | |||||
| | | * | | New directive hardtest and hardcheck to run on hardware test/mppa/instr | Cyril SIX | 2020-01-27 | 1 | -11/+55 |
| | | | | | |||||
| | * | | | Tail duplication optimization defaulting to off | Cyril SIX | 2020-01-27 | 2 | -2/+1 |
| | | | | | |||||
| | * | | | Added a flag to desactivate tail duplication | Cyril SIX | 2020-01-27 | 5 | -6/+17 |
| | | | | | |||||
| | * | | | Added debug message when inverting ifso ifnot | Cyril SIX | 2020-01-24 | 1 | -1/+3 |
| | | | | | |||||
| | * | | | Oracle inverting branches when trace does not go in fallthru | Cyril SIX | 2020-01-24 | 1 | -2/+21 |
| | | | | | |||||
| | * | | | Revert "Modified the hook for the oracle" | Cyril SIX | 2020-01-23 | 3 | -12/+8 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 04a46f516487557df00f43453c8decbc8567c458. It was actually not needed | ||||
| | * | | | Verificator finished for handling reversed Icond | Cyril SIX | 2020-01-23 | 2 | -11/+18 |
| | | | | | |||||
| | * | | | Added clause in match_inst to allow Icond reversal | Cyril SIX | 2020-01-23 | 1 | -4/+13 |
| | | | | | |||||
| | * | | | Modified the hook for the oracle | Cyril SIX | 2020-01-23 | 3 | -8/+12 |
| | | | | | |||||
| | * | | | Fixing bug caused by get_predecessors returning duplicates | Cyril SIX | 2020-01-23 | 1 | -5/+8 |
| | | | | | |||||
| | * | | | Printing traces right before duplicating | Cyril SIX | 2020-01-23 | 1 | -5/+2 |
| | | | | | |||||
| | * | | | Fixing bug (used physical instead of structural inequality) | Cyril SIX | 2020-01-22 | 1 | -1/+2 |
| | | | | | |||||
| | * | | | Merge branch 'mppa-work' into mppa-duplicate-oracle | Cyril SIX | 2020-01-22 | 26 | -68/+1905 |
| | |\| | | |||||
| | * | | | Fixing is_empty function | Cyril SIX | 2020-01-22 | 1 | -3/+3 |
| | | | | | |||||
| | * | | | Branch duplication implementation | Cyril SIX | 2020-01-22 | 1 | -12/+94 |
| | | | | | |||||
| | * | | | Set up the groundbase for doing the duplication | Cyril SIX | 2020-01-17 | 1 | -4/+14 |
| | | | | | |||||
| | * | | | Removed unnecessary .mli file (provoked compilation problems) | Cyril SIX | 2020-01-17 | 1 | -12/+0 |
| | | | | | |||||
| | * | | | Adding more debug elements | Cyril SIX | 2020-01-15 | 1 | -1/+9 |
| | | | | | |||||
| | * | | | Typo in printf | Cyril SIX | 2020-01-13 | 1 | -1/+1 |
| | | | | | |||||
| | * | | | Opcode heuristic done for K1c | Cyril SIX | 2019-12-16 | 3 | -3/+33 |
| | | | | | |||||
| | * | | | Stub for opcode heuristic | Cyril SIX | 2019-12-16 | 3 | -4/+16 |
| | | | | | |||||
| | * | | | Fixing loop heuristic for the way CompCert handles loops | Cyril SIX | 2019-12-11 | 1 | -11/+19 |
| | | | | |