Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Compiler options to manage expansions | Léo Gourdin | 2021-03-26 | 2 | -2/+2 |
| | |||||
* | Adding a flag to test fp_init_exp | Léo Gourdin | 2021-03-02 | 2 | -0/+2 |
| | |||||
* | Adding a compiler option -fexpanse-rtlcond | Léo Gourdin | 2021-02-16 | 2 | -0/+2 |
| | |||||
* | Conditions now propagated by CSE3 | David Monniaux | 2021-01-20 | 3 | -1/+8 |
|\ | | | | | | | Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work | ||||
| * | begin implementing -fcse3-conditions | David Monniaux | 2020-12-09 | 3 | -0/+7 |
| | | |||||
| * | CSE3 compiles again, but some admitted lemmas | David Monniaux | 2020-12-09 | 1 | -1/+1 |
| | | |||||
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3 | David Monniaux | 2020-12-08 | 7 | -229/+51 |
| |\ | |||||
| * | | start checking for bugs | David Monniaux | 2020-12-02 | 1 | -1/+1 |
| | | | |||||
* | | | Fix --help for prepass (new options) | Léo Gourdin | 2021-01-14 | 1 | -1/+1 |
| | | | |||||
* | | | Fix --help for prepass (default on) | Léo Gourdin | 2021-01-14 | 1 | -1/+1 |
| | | | |||||
* | | | Merge branch 'kvx-work' into aarch64-peephole | Sylvain Boulmé | 2020-12-17 | 7 | -229/+51 |
|\ \ \ | | |/ | |/| | |||||
| * | | Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixed | David Monniaux | 2020-12-08 | 1 | -0/+2 |
| |\ \ | |||||
| | * | | Error when using -main without -interp | Xavier Leroy | 2020-12-06 | 1 | -0/+2 |
| | | | | | | | | | | | | | | | | | | | | | | | | Outside of -interp mode, -main has no (known) effect but could be confused for a linker option that sets the program's entrypoint, say. It's safer to reject the option. | ||||
| * | | | Merge branch 'kvx-work' into kvx-work-merge3.8 | Cyril SIX | 2020-12-04 | 3 | -2/+24 |
| |\ \ \ | | | |/ | | |/| | | | | | | | | | | | | | Conflicts: Makefile configure | ||||
| * | | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8 | David Monniaux | 2020-11-18 | 7 | -229/+49 |
| |\ \ \ | | | |/ | | |/| | |||||
| | * | | Add -main option to specify entrypoint function in interpreter mode (#374) | Xavier Leroy | 2020-10-30 | 3 | -19/+41 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | When running unit tests with the CompCert reference interpreter, it's nice to be able to start execution at a given test function instead of having to write a main function. This PR adds a -main command-line option to give the name of the entry point function. The default is still main. Frama-C has a similar option. The function specified with -main is called with no arguments. If its return type is int, its return value is the exit status of the program. Otherwise, its return value is ignored and the program exits with status 0. | ||||
| | * | | Remove -version-file option | Xavier Leroy | 2020-10-12 | 1 | -19/+2 |
| | | | | | | | | | | | | | | | | It is specific to AbsInt's commercial version of CompCert. | ||||
| | * | | Add missing comment for print_version_file_and_exit | Christoph Cullmann | 2020-07-30 | 1 | -0/+1 |
| | | | | |||||
| | * | | No trailing commas for --version-file option. | Bernhard Schommer | 2020-07-09 | 1 | -1/+1 |
| | | | | |||||
| | * | | Fix typo. | Bernhard Schommer | 2020-07-08 | 1 | -1/+1 |
| | | | | |||||
| | * | | Revert "Use the same version string." | Bernhard Schommer | 2020-07-08 | 1 | -3/+10 |
| | | | | | | | | | | | | | | | | This reverts commit 1a01ad629109cdb60fddae3787e3a589d20e9790. | ||||
| | * | | Use the same version string. | Bernhard Schommer | 2020-07-08 | 1 | -10/+3 |
| | | | | | | | | | | | | | | | | | | | | | | | | The version string dumped in the file should be the same as the version string printed by `-version`. The option is also not printed by `-help` since it is for internal use only. | ||||
| | * | | Remove no longer needed option enforce-buildnr | Bernhard Schommer | 2020-07-08 | 1 | -10/+1 |
| | | | | |||||
| | * | | Introduce additional "branch" build information. | Bernhard Schommer | 2020-07-08 | 1 | -3/+5 |
| | | | | |||||
| | * | | Add option to print version information in file | Bernhard Schommer | 2020-07-08 | 1 | -1/+17 |
| | | | | |||||
| | * | | Move Commandline to the lib/ directory | Xavier Leroy | 2020-05-05 | 2 | -196/+0 |
| | | | | | | | | | | | | | | | | | | | | | | | | The Commandline module is reusable in other projects, and its license (GPL) allows such reuse, so its natural place is in lib/ rather than in driver/ | ||||
| | * | | Move reserved_registers to CPragmas. | Bernhard Schommer | 2020-04-20 | 1 | -0/+1 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | The list of reserved_registers is never reset between the compilation of multiple files. Instead of storing them in IRC they are moved in the CPragmas file and reset in the a new reset function for Cpragmas whic is called per file. | ||||
* | | | | set prepass by default | David Monniaux | 2020-11-27 | 1 | -1/+1 |
| |_|/ |/| | | |||||
* | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-19 | 1 | -1/+1 |
|\ \ \ | |||||
| * | | | Tunneling: improved elimination of conditions | Sylvain Boulmé | 2020-11-16 | 1 | -1/+1 |
| |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously, the elimination of useless conditions done in the 2nd pass of the tunneling introduced some new "nop" instructions that were not eliminated. This commit solves this issue by anticipating the elimination of conditions in the 1st pass of the tunneling, the 2nd pass being unchanged. In case of cycles in the CFG, the full elimination of useless conditions may require several iterations in the 1st pass. Moreover, in the simulation proof, the measure counting the number of eliminated steps from each node, needs to be adapted according to the modifications on the 1st pass. Hence, this measure results from a quite complex fixpoint computation: proving its properties would be very difficult. This leads us to introduce an oracle, implementing the first pass and producing the expected measure. A certified verifier directly checks that the measure provided by the oracle satisfies the properties expected by the simulation proof. Introducing this oracle/verifier pair has here the following advantage: - the proof is simpler than the original one (e.g. having a certified union-find structure is no more necessary for this pass). - the oracle is very efficient, by using imperative data-structure to compute memoized fixpoints. At runtime, the overhead induced by the verifier computations (and the actual computation of the measure) seems largely compensated by the gains obtained through the imperative oracle. | ||||
* | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-03 | 2 | -0/+4 |
|\| | | |||||
| * | | Loop Rotate with -flooprotate | Cyril SIX | 2020-11-03 | 2 | -0/+4 |
| | | | |||||
* | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-31 | 2 | -0/+3 |
|\| | | |||||
| * | | refining CSE3 nodes | David Monniaux | 2020-10-31 | 2 | -0/+3 |
| | | | |||||
| * | | deactivate LICM | David Monniaux | 2020-10-28 | 1 | -1/+1 |
| | | | |||||
* | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-27 | 1 | -0/+1 |
|\| | | |||||
| * | | Merge branch 'kvx-work' into duplicate-param | Cyril SIX | 2020-10-27 | 3 | -0/+7 |
| |\ \ | |||||
| * | | | Reworked Duplicate to be parametrized | Cyril SIX | 2020-10-27 | 1 | -0/+1 |
| | | | | |||||
* | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-27 | 3 | -0/+7 |
|\ \ \ \ | | |/ / | |/| | | |||||
| * | | | new option for CSE3 (trivial ops) | David Monniaux | 2020-10-27 | 3 | -0/+7 |
| |/ / | |||||
* | | | deactivate LICM by default | David Monniaux | 2020-10-27 | 1 | -1/+1 |
| | | | |||||
* | | | -mtune= | David Monniaux | 2020-10-22 | 2 | -1/+5 |
| | | | |||||
* | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-18 | 3 | -17/+22 |
|\| | | |||||
| * | | Loop body unrolling with -funrollbody n | Cyril SIX | 2020-10-16 | 2 | -0/+3 |
| | | | |||||
| * | | -O0 desactivates -fpredict and -ftracelinearize | Cyril SIX | 2020-10-14 | 1 | -0/+1 |
| | | | |||||
| * | | Updated --help | Cyril SIX | 2020-10-14 | 1 | -9/+5 |
| | | | |||||
| * | | new flags: -fpredict, -ftailduplicate n, -funrollsingle n instead of just ↵ | Cyril SIX | 2020-10-09 | 2 | -5/+10 |
| | | | | | | | | | | | | -fduplicate n | ||||
| * | | Changing duplicate verifier to be non optional | Cyril SIX | 2020-10-09 | 1 | -3/+0 |
| | | | |||||
* | | | command line selection of prepass scheduler | David Monniaux | 2020-07-11 | 2 | -0/+4 |
| | | | |||||
* | | | use a command-line option | David Monniaux | 2020-07-08 | 2 | -1/+4 |
| | | |