aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
...
* | Merge remote-tracking branch 'refs/remotes/origin/mppa-duplicate-oracle' ↵Cyril SIX2019-12-094-130/+11
|\ \ | | | | | | | | | into mppa-duplicate-oracle
| * | Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into ↵David Monniaux2019-12-094-130/+11
| |\| | | | | | | | | | mppa-duplicate-oracle
| | * Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-mergeDavid Monniaux2019-12-0949-157/+1158
| | |\
| | * | merge merge mergeDavid Monniaux2019-11-141-1/+1
| | | |
| | * | Merge branch 'mppa-work-upstream-merge' of ↵David Monniaux2019-11-141-3/+1
| | |\ \ | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work-upstream-merge
| | | * \ Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-mergeDavid Monniaux2019-11-144-0/+710
| | | |\ \
| | * | \ \ Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-mergeDavid Monniaux2019-11-142-187/+154
| | |\ \ \ \ | | | | |/ / | | | |/| |
| | * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-11-135-126/+11
| | |\ \ \ \ | | | | | | | | | | | | | | | | | | | | | mppa-work-upstream-merge
| | | * | | | Remove no longer needed file PrintLTLinBernhard Schommer2019-11-121-115/+0
| | | | | | |
| | | * | | | Make explicit the use of hints from OrderedType (#316)Vincent Laporte2019-10-022-8/+8
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Some hints will move from the core database to the `ordered_type` database (see https://github.com/coq/coq/pull/9772). This commit prepares for this move by adding `with ordered_type` to the invocations of `auto` and `eauto` that use the hints in question.
| | * | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-mergeDavid Monniaux2019-11-134-1/+740
| | |\ \ \ \ \ | | | |_|_|/ / | | |/| | | |
* | / | | | | Rajout du calcul de dominateurs - pas testéCyril SIX2019-12-091-16/+43
|/ / / / / /
* | | | | | merge w/ non trapping loadsDavid Monniaux2019-12-061-3/+3
| | | | | |
* | | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-duplicate-oracleDavid Monniaux2019-12-0658-423/+1502
|\ \ \ \ \ \ | | |_|_|_|/ | |/| | | |
| * | | | | make it compile for ARMDavid Monniaux2019-12-061-4/+4
| | | | | |
| * | | | | finish mergeDavid Monniaux2019-12-023-14/+32
| | | | | |
| * | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-024-1/+709
| |\ \ \ \ \
| | * | | | | Duplicateproof: minor editSylvain Boulmé2019-11-261-3/+4
| | | |_|_|/ | | |/| | |
| | * | | | simplification of Duplicate: remove xfunctionSylvain Boulmé2019-11-142-187/+154
| | | |/ / | | |/| |
| | * | | Merge remote-tracking branch 'origin/mppa-duplicate-rtl-alt' into mppa-workCyril SIX2019-10-242-60/+77
| | |\ \ \
| | | * | | An alternative proof where the match_state does not depend on the translationSylvain Boulmé2019-10-232-60/+77
| | | | | |
| | * | | | eq_condition already existedDavid Monniaux2019-10-162-2/+2
| | | | | |
| | * | | | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-1610-51/+146
| | |\ \ \ \ | | | |/ / / | | |/| | / | | | | |/ | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: .gitignore backend/Lineartyping.v common/Values.v configure cparser/Machine.ml cparser/Machine.mli driver/Configuration.ml driver/Frontend.ml runtime/Makefile test/c/Makefile test/c/aes.c test/compression/Makefile test/regression/Makefile test/regression/extasm.c test/regression/floats-basics.c test/regression/floats.c Note : test/regression should be checked, didn't test it yet
| * | | | Merge tag 'v3.6_mppa_2019-09-20' of ↵David Monniaux2019-09-2010-54/+148
| |\ \ \ \ | | | |_|/ | | |/| | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load
| | * | | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-09-2010-54/+148
| | |\ \ \ | | | | |/ | | | |/| | | | | | mppa-work-upstream-merge
| | | * | Reworked json export.Bernhard Schommer2019-09-123-29/+37
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The json export prints formatted json, which takes a lot of additional time, however the result is only consumed by other tools and not meant for human reading. This commit implements several small changes in order to speedup the json export: * Removal of usage of the Format Module * Replacing `fprintf` calls by calls to function that print directly, such as `output_string`, etc. * Replacing list of all instruction names by a set of all instructions
| | | * | Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-2/+2
| | | | | | | | | | | | | | | Some changes were not correctly propagated to all architectures.
| | | * | AArch64 portXavier Leroy2019-08-087-37/+97
| | | | | | | | | | | | | | | | | | | | | | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
| | | * | Asmgenproof0: add predicate exec_straight0Xavier Leroy2019-08-071-0/+26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a variant of exec_straight where it is allowed to take zero steps. In other words, exec_straight0 is the "star" relation, while exec_straight is the "plus" relation. In the end we need "plus" relations in simulation diagrams, to show the absence of stuttering. But the "star" relation exec_straight0 is useful to reason about code fragments that are always preceded or followed by at least one instruction.
| | | * | Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-071-2/+0
| | | | | | | | | | | | | | | | | | | | | | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core".
| * | | | missing fileDavid Monniaux2019-09-091-0/+26
| | | | |
| * | | | proof for AllnontrapDavid Monniaux2019-09-091-0/+215
| | | | |
| * | | | finished the proofs for non-trapping loadsDavid Monniaux2019-09-081-10/+21
| | | | |
| * | | | fixes for compiling on other platformsDavid Monniaux2019-09-074-8/+8
| | | | |
| * | | | fixes for ARMDavid Monniaux2019-09-074-21/+12
| | | | |
| * | | | notrap works on x86David Monniaux2019-09-071-12/+3
| | | | |
| * | | | more for passing notrap through x86David Monniaux2019-09-071-2/+10
| | | | |
| * | | | ONE "admitted" and things compileDavid Monniaux2019-09-0611-46/+83
| | | | |
| * | | | progress in proofDavid Monniaux2019-09-051-14/+27
| | | | |
| * | | | BSload notrap1David Monniaux2019-09-051-1/+19
| | | | |
| * | | | moving forward with proofsDavid Monniaux2019-09-052-29/+29
| | | | |
| * | | | more proofsDavid Monniaux2019-09-051-0/+39
| | | | |
| * | | | more on notrapDavid Monniaux2019-09-052-5/+18
| | | | |
| * | | | more proofDavid Monniaux2019-09-051-0/+16
| | | | |
| * | | | some more proofs on notrapDavid Monniaux2019-09-051-0/+12
| | | | |
| * | | | more proofs going throughDavid Monniaux2019-09-059-26/+95
| | | | |
| * | | | LinearizeProof for non trapping loadsDavid Monniaux2019-09-051-16/+32
| | | | |
| * | | | CSEproof for non trapping loadsDavid Monniaux2019-09-053-19/+89
| | | | |
| * | | | going forwardDavid Monniaux2019-09-041-41/+50
| | | | |
| * | | | stuck in CSEproofDavid Monniaux2019-09-041-1/+10
| | | | |
generated by cgit (git 2.34.1) at 2024-07-14 10:27:44 +0000