aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Clflags.ml
Commit message (Collapse)AuthorAgeFilesLines
* Adding both RV expansion methods in kvx-workLéo Gourdin2021-05-191-0/+2
|
* Remove flagsLéo Gourdin2021-04-091-2/+0
|
* Compiler options to manage expansionsLéo Gourdin2021-03-261-1/+1
|
* Adding a flag to test fp_init_expLéo Gourdin2021-03-021-0/+1
|
* Adding a compiler option -fexpanse-rtlcondLéo Gourdin2021-02-161-0/+1
|
* Conditions now propagated by CSE3David Monniaux2021-01-201-1/+3
|\ | | | | | | Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work
| * begin implementing -fcse3-conditionsDavid Monniaux2020-12-091-0/+2
| |
| * CSE3 compiles again, but some admitted lemmasDavid Monniaux2020-12-091-1/+1
| |
| * Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-081-0/+1
| |\
| * | start checking for bugsDavid Monniaux2020-12-021-1/+1
| | |
* | | Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-171-0/+1
|\ \ \ | | |/ | |/|
| * | Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-041-0/+7
| |\| | | | | | | | | | | | | | | | Conflicts: Makefile configure
| * | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-0/+1
| |\ \
| | * | Add -main option to specify entrypoint function in interpreter mode (#374)Xavier Leroy2020-10-301-0/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | set prepass by defaultDavid Monniaux2020-11-271-1/+1
| |_|/ |/| |
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-031-0/+1
|\| |
| * | Loop Rotate with -flooprotateCyril SIX2020-11-031-0/+1
| | |
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-311-0/+1
|\| |
| * | refining CSE3 nodesDavid Monniaux2020-10-311-0/+1
| | |
| * | deactivate LICMDavid Monniaux2020-10-281-1/+1
| | |
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-271-0/+2
|\| |
| * | new option for CSE3 (trivial ops)David Monniaux2020-10-271-0/+2
| | |
* | | deactivate LICM by defaultDavid Monniaux2020-10-271-1/+1
| | |
* | | -mtune=David Monniaux2020-10-221-0/+2
| | |
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-181-3/+11
|\| |
| * | Loop body unrolling with -funrollbody nCyril SIX2020-10-161-0/+1
| | |
| * | new flags: -fpredict, -ftailduplicate n, -funrollsingle n instead of just ↵Cyril SIX2020-10-091-3/+7
| | | | | | | | | | | | -fduplicate n
* | | command line selection of prepass schedulerDavid Monniaux2020-07-111-0/+1
| | |
* | | use a command-line optionDavid Monniaux2020-07-081-0/+1
|/ /
* | k1c -> kvx changesDavid Monniaux2020-05-261-1/+1
| |
* | -fcse3-glbDavid Monniaux2020-05-061-0/+1
| |
* | CSE3 across mergesDavid Monniaux2020-05-061-0/+1
| |
* | Merge branch 'mppa-work' of ↵David Monniaux2020-04-231-2/+13
|\ \ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * \ Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-231-2/+3
| |\ \
| | * | CSE3 across callsDavid Monniaux2020-04-231-1/+2
| | | |
| | * | Merge remote-tracking branch 'origin/mppa-cse3' into mppa-licmDavid Monniaux2020-04-231-0/+1
| | |\ \
| | | * | make tracing output optionalDavid Monniaux2020-04-231-0/+1
| | | | |
| * | | | Merge remote-tracking branch 'origin/mppa-fast-div' into mppa-featuresDavid Monniaux2020-04-201-0/+2
| |\ \ \ \
| | * \ \ \ Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-divDavid Monniaux2020-04-201-2/+12
| | |\ \ \ \ | | | | | | | | | | | | | | | | | | | | | (unfinished)
| | * | | | | added -fdiv-i32 and -fdiv-i64 optionsDavid Monniaux2019-05-291-0/+3
| | | | | | |
| * | | | | | Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-201-1/+4
| |\ \ \ \ \ \ | | | |_|/ / / | | |/| | | |
| | * | | | | add options for controlling madd and notrap selectionDavid Monniaux2020-04-191-1/+3
| | | | | | |
| | * | | | | activate LICMDavid Monniaux2020-04-191-1/+1
| | | | | | |
| | * | | | | begin adapting for LICM phaseDavid Monniaux2020-04-011-0/+1
| | | |_|/ / | | |/| | |
| * | | | | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-121-0/+3
| |\ \ \ \ \ | | |/ / / / | |/| | | |
| | * | | | reloading and exploiting seems to workDavid Monniaux2020-04-081-0/+1
| | | | | |
| | * | | | fixed a bug in support libraries; reload profiling infoDavid Monniaux2020-04-081-1/+0
| | | | | |
| | * | | | begin installing profilingDavid Monniaux2020-04-081-0/+3
| | | |/ / | | |/| |
| * | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-171-1/+1
| |\| | |
| * | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-151-0/+1
| |\ \ \ \
generated by cgit (git 2.34.1) at 2024-07-14 02:51:02 +0000