aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | ca avanceDavid Monniaux2019-09-041-2/+11
| | | |
| * | | begin CSE proof for notrap loadDavid Monniaux2019-09-041-3/+85
| | | |
| * | | begin CSEDavid Monniaux2019-09-044-18/+23
| | | |
| * | | moved trapping_mode to a more appropriate placeDavid Monniaux2019-09-031-2/+0
| | | |
| * | | Dead code proof for non trapping loadsDavid Monniaux2019-09-031-0/+77
| | | |
| * | | finished Constopproof for non trapping loadsDavid Monniaux2019-09-031-1/+41
| | | |
| * | | advancing in constant propagationDavid Monniaux2019-09-032-2/+22
| | | |
| * | | Value analysis for non trapping loadsDavid Monniaux2019-09-032-4/+38
| | | |
| * | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-0319-134/+439
| |\ \ \
| * | | | progress on non trapping loadsDavid Monniaux2019-09-031-0/+54
| | | | |
| * | | | progress on non trapping loadsDavid Monniaux2019-09-021-8/+32
| | | | |
| * | | | avancement (il faut utiliser Vundef visiblement)David Monniaux2019-09-0218-41/+114
| | | | |
* | | | | 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
|\ \ \ \ \ | | |/ / / | |/| | |
| * | | | simplification of Duplicate: remove xfunctionSylvain Boulmé2019-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
|\ \ \ \ \ \ | | |/ / / / | |/| / / / | |_|/ / / |/| | | |
| * | | | 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
| * | | | Finished Duplicate proof.Cyril SIX2019-10-072-36/+58
| | | | |
| * | | | IcondCyril SIX2019-10-072-0/+26
| | | | |
| * | | | Fixing identity PTree in Duplicateaux oracleCyril SIX2019-10-071-2/+8
| | | | |
| * | | | ItailcallCyril SIX2019-10-072-2/+17
| | | | |
| * | | | IreturnCyril SIX2019-10-072-1/+9
| | | | |
| * | | | Ibuiltin proofCyril SIX2019-10-042-0/+31
| | | | |
| * | | | IcallCyril SIX2019-10-032-0/+27
| | | | |
| * | | | Iload and IstoreCyril SIX2019-10-032-3/+43
| | | | |
| * | | | Proof for IopCyril SIX2019-10-032-1/+20
| | | | |
| * | | | Preparing the terrain for the rest of the instructions with one successorCyril SIX2019-10-031-5/+17
| | | | |
| * | | | Duplicate - Proof of verificator for InopCyril SIX2019-10-032-4/+83
| | | | |
| * | | | Starting implementing the verificatorCyril SIX2019-10-022-1/+34
| | | | |
| * | | | Identity oracle realizing verify_mapping_entrypointCyril SIX2019-10-021-1/+4
| | | | |
| * | | | Proof of first axiomCyril SIX2019-09-112-4/+25
| | | | |
| * | | | Fixing Linking problemCyril SIX2019-09-112-31/+31
| | | | |
| * | | | Utilisation d'un intermédiaire xfunction contenant le revmapCyril SIX2019-09-112-47/+81
| | | | |
| * | | | Duplicate: proof complete, assuming revmap, revmap_correct and revmap_entrypointCyril SIX2019-09-061-5/+21
| | | | |
| * | | | Duplicate: big progress on step_simulation, only Ijumptbl leftCyril SIX2019-09-053-85/+148
| | | | |
| * | | | Duplicate: changement de match_nodesCyril SIX2019-09-041-36/+44
| | | | |
| * | | | Duplicate: exec_function_external et exec_returnCyril SIX2019-09-041-3/+7
| | | | |
| * | | | Duplicate: exec_function_internalCyril SIX2019-09-042-2/+43
| | | | |
| * | | | transf_initial_statesCyril SIX2019-09-043-12/+84
| | | | |
| * | | | Duplicate: match_statesCyril SIX2019-09-031-2/+10
| | | | |
| * | | | Duplicate: match_nodesCyril SIX2019-09-031-8/+57
| | | | |
| * | | | Start of match_statesCyril SIX2019-09-031-3/+23
| | | | |
generated by cgit (git 2.34.1) at 2024-07-12 04:50:50 +0000