| Commit message (Expand) | Author | Age | Files | Lines | ||
|---|---|---|---|---|---|---|
| ... | ||||||
| | | | * | Added dwarf register numbers for aarch64 | Bernhard Schommer | 2019-11-28 | 1 | -3/+18 | |
| | | | * | Added back unused_ais_parameter warning. | Bernhard Schommer | 2019-11-26 | 1 | -0/+1 | |
| | | | * | Simplified diagnostics module. | Bernhard Schommer | 2019-11-25 | 1 | -118/+41 | |
| | | * | | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-merge | David Monniaux | 2019-12-09 | 101 | -471/+2379 | |
| | | |\ \ | ||||||
| | | * \ \ | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-merge | David Monniaux | 2019-11-24 | 11 | -248/+664 | |
| | | |\ \ \ | ||||||
| | | * | | | | merge merge merge | David Monniaux | 2019-11-14 | 1 | -1/+1 | |
| | | * | | | | Merge branch 'mppa-work-upstream-merge' of gricad-gitlab.univ-grenoble-alpes.... | David Monniaux | 2019-11-14 | 1 | -3/+1 | |
| | | |\ \ \ \ | ||||||
| | | | * \ \ \ | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-merge | David Monniaux | 2019-11-14 | 101 | -2786/+3968 | |
| | | | |\ \ \ \ | ||||||
| | | * | \ \ \ \ | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-merge | David Monniaux | 2019-11-14 | 5 | -195/+168 | |
| | | |\ \ \ \ \ \ | | | | |/ / / / | | | |/| | | | | ||||||
| | | * | | | | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up... | David Monniaux | 2019-11-13 | 19 | -165/+89 | |
| | | |\ \ \ \ \ \ | | | | |_|_|_|/ | | | |/| | | | | ||||||
| | | | * | | | | | Remove no longer needed file PrintLTLin | Bernhard Schommer | 2019-11-12 | 1 | -115/+0 | |
| | | | * | | | | | Use `intuition idtac` instead of `intuition` (#321) | Vincent Laporte | 2019-11-12 | 1 | -1/+1 | |
| | | | * | | | | | Raise minimal required versions for OCaml and Coq (#203) | Bernhard Schommer | 2019-10-31 | 1 | -9/+4 | |
| | | | * | | | | | More robust proof of `size_and` (#320) | Frédéric Besson | 2019-10-30 | 1 | -4/+5 | |
| | | | * | | | | | Add support for Coq 8.10.1 | Xavier Leroy | 2019-10-28 | 1 | -2/+2 | |
| | | | * | | | | | clightgen: sanitize names of functions and global variables | Xavier Leroy | 2019-10-28 | 2 | -4/+16 | |
| | | | * | | | | | Fix configure for coq 8.10.0 | Michael Schmidt | 2019-10-13 | 1 | -2/+2 | |
| | | | * | | | | | Make explicit the use of hints from OrderedType (#316) | Vincent Laporte | 2019-10-02 | 4 | -15/+17 | |
| | | | * | | | | | Remove duplicated ticks. | Bernhard Schommer | 2019-10-01 | 1 | -2/+2 | |
| | | | * | | | | | Use pointer type for evaluated constants. | Bernhard Schommer | 2019-10-01 | 1 | -1/+1 | |
| | | | * | | | | | Various improvements for diagnostics. | Bernhard Schommer | 2019-09-30 | 3 | -10/+34 | |
| | | | * | | | | | Added .gitattributes file. | Bernhard Schommer | 2019-09-30 | 1 | -0/+3 | |
| | | | * | | | | | Functions that are extern should stay extern (#201) | Bernhard Schommer | 2019-09-25 | 1 | -1/+1 | |
| | | | * | | | | | Model GPR0 in isel (#199) | Xavier Leroy | 2019-09-17 | 2 | -2/+4 | |
| | | * | | | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-merge | David Monniaux | 2019-11-13 | 99 | -2780/+3982 | |
| | | |\ \ \ \ \ \ | | | |_|_|/ / / | | |/| | | | | | ||||||
| * | / | | | | | | Rajout du calcul de dominateurs - pas testé | Cyril SIX | 2019-12-09 | 1 | -16/+43 | |
| |/ / / / / / / | ||||||
| * | | | | | | | merge w/ non trapping loads | David Monniaux | 2019-12-06 | 1 | -3/+3 | |
| * | | | | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-duplicate-oracle | David Monniaux | 2019-12-06 | 199 | -3768/+22046 | |
| |\ \ \ \ \ \ \ | | |_|_|_|_|/ | |/| | | | | | ||||||
| | * | | | | | | make it compile for ARM | David Monniaux | 2019-12-06 | 1 | -4/+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 | 6 | -56/+71 | |
| | * | | | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load | David Monniaux | 2019-12-02 | 53 | -601/+1855 | |
| | |\ \ \ \ \ \ | ||||||
| | | * | | | | | | Adding info on how to add timings to a benchmark | Cyril SIX | 2019-12-02 | 1 | -26/+44 | |
| | | * | | | | | | Updating test/monniaux/README.md | Cyril SIX | 2019-11-26 | 1 | -28/+39 | |
| | | * | | | | | | build_benches.sh adapting to number of cores | Cyril SIX | 2019-11-26 | 1 | -2/+3 | |
| | | * | | | | | | run-benches.sh adapting to number of CPU cores | Cyril SIX | 2019-11-26 | 1 | -1/+4 | |
| | | * | | | | | | Duplicateproof: minor edit | Sylvain Boulmé | 2019-11-26 | 1 | -3/+4 | |
| | | | |_|_|_|/ | | |/| | | | | ||||||
| | | * | | | | | Fixing pcre2 (but it is bugged in GCC?) | Cyril SIX | 2019-11-22 | 2 | -36/+5 | |
| | | * | | | | | benches += ncompress | Cyril SIX | 2019-11-22 | 2 | -52/+4 | |
| | | * | | | | | Real clean | Cyril SIX | 2019-11-22 | 1 | -1/+1 | |
| | | * | | | | | benches += tiff | Cyril SIX | 2019-11-22 | 3 | -49/+4 | |
| | | * | | | | | Adding the new benches to benches.sh | Cyril SIX | 2019-11-22 | 1 | -1/+1 | |
| | | * | | | | | benchmarks += ocaml | Cyril SIX | 2019-11-22 | 1 | -30/+3 | |
| | | * | | | | | Fixing zlib | Cyril SIX | 2019-11-19 | 3 | -0/+541 | |
| | | * | | | | | Adding zlib | Cyril SIX | 2019-11-15 | 1 | -49/+57 | |
| | | * | | | | | Adding jpeg-6b benchmark | Cyril SIX | 2019-11-15 | 2 | -32/+50 | |
| | | | |_|_|/ | | |/| | | | ||||||
| | | * | | | | simplification of Duplicate: remove xfunction | Sylvain Boulmé | 2019-11-14 | 2 | -187/+154 | |
| | | * | | | | fixing a potential inconsistency from unsafe_coerce | Sylvain Boulmé | 2019-11-14 | 2 | -7/+13 | |
| | | * | | | | removing Focus (deprecated) | Sylvain Boulmé | 2019-11-14 | 1 | -2/+2 | |
| | | * | | | | Correcting typo in rules.mk | Cyril SIX | 2019-11-13 | 1 | -1/+1 | |
| | | | |/ / | | |/| | | ||||||
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |