| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | 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 | ||||
| | | * | Added base address if needed. | Bernhard Schommer | 2020-02-06 | 3 | -33/+53 |
| | | | | | | | | | | | | | | | | | | | | | | | | | Ranges of locations are relative to some base address. Most times this is just the same as the compilation unit. However if the compilation unit contains functions in multiple sections we need to add a base address of the section that the locations are contained. | ||||
| | | * | Compatibility with OCaml 4.10 (#214) | Xavier Leroy | 2020-02-06 | 3 | -7/+7 |
| | | | | | | | | | | | | | | | | | | | | | | | | | debug/DwarfPrinter.mli: unused functor parameter trigger warning 69, replace by non-dependent functor type. Makefile.extr: turn warning 69 (unused functor parameter) off for extracted code configure: accept OCaml versions above 4.09 configure: update messages for unsupported versions of OCaml and Coq | ||||
| | | * | Revised menhirLib autoconfiguration (#331) | Xavier Leroy | 2020-02-05 | 3 | -5/+9 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since Menhir version 20200123, we need to link with menhirLib.cmxa instead of menhirLib.cmx. This commit chooses automatically the file to link with: menhirLib.cmxa if it exists in the menhirLib installation directory, menhirLib.cmx otherwise. To reliably find the installation directory, configure was changed to record the menhirLib directory in Makefile.config, variable MENHIR_DIR, instead of a pre-cooked command-line option MENHIR_INCLUDES. Makefile.extr was adapted accordingly. Fixes: #329 Closes: #330 | ||||
| | | * | Support Coq 8.11.0 (#212) | Xavier Leroy | 2020-02-05 | 4 | -2/+8 |
| | | | | | | | | | | | | | Update configure. Ignore and clean up .vok and .vos files, which Coq 8.11.0 generates. | ||||
| | | * | Incorrect computation of extra stack size for vararg calls in RISC-V (#213) | Bernhard Schommer | 2020-02-05 | 1 | -2/+2 |
| | | | | | | | | | | | | | | | | Currently, the extra size for the variable arguments is too small for the 64 bit RISC-V and the extra arguments are stored in the wrong stack slots. | ||||
| | | * | Reduce the checking time for the "decidable_equality_from" tactic | xavier.leroy | 2020-01-30 | 1 | -4/+5 |
| | | | | | | | | | | | | | Just moved a frequent failure case ahead of a costly "simpl". | ||||
| | * | | 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 |
| | | | | | |||||
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |