aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* | | | Few minor other changes in proofCyril SIX2019-10-151-3/+3
* | | | More elaborate comments + rewriting for easier to understand Asmblockgenproof.vCyril SIX2019-10-151-145/+89
* | | | Fix for test/regression/struct2.cCyril SIX2019-10-141-1/+2
* | | | Tackling struct passing by value for the future K1C ABICyril SIX2019-10-143-2/+12
* | | | Explicitly naming SP_split_args for easier greppingCyril SIX2019-10-141-1/+1
* | | | Converting mppa_k1c/*.v files to Unix formatCyril SIX2019-10-112-754/+754
* | | | Fixing fp_is_parent too weak (#165)Cyril SIX2019-10-112-1798/+1811
* | | | Removing Coq 8.7.* in configure (not compatible with "3: {..}" directives)Cyril SIX2019-10-091-2/+2
* | | | Merge branch 'mppa-duplicate-rtl' into mppa-workCyril SIX2019-10-089-31/+876
|\ \ \ \ | | |_|/ | |/| |
| * | | Finished Duplicate proof.Cyril SIX2019-10-072-36/+58
| * | | IcondCyril SIX2019-10-074-0/+37
| * | | 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-045-13/+138
| * | | Adding decidable equality for intCyril SIX2019-10-041-1/+12
| * | | 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
| * | | Merge branch 'mppa-work' into mppa-duplicate-rtlCyril SIX2019-10-0269-142/+1040
| |\ \ \
| * | | | 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
| * | | | Stubs for Duplicate passCyril SIX2019-09-035-28/+100
* | | | | genann addedCyril SIX2019-10-023-3/+5
* | | | | Adding picosat to the benchesCyril SIX2019-10-022-34/+8
* | | | | Updating test/monniaux/README.mdCyril SIX2019-10-021-1/+8
* | | | | (forgot to add glpk to benches.sh)Cyril SIX2019-10-021-1/+1
* | | | | Intégration de GLPKCyril SIX2019-10-022-37/+7
* | | | | Asmblockgenproof : cur rewritingCyril SIX2019-10-011-11/+11
* | | | | Tiny cleanCyril SIX2019-10-011-1/+0
* | | | | Asmblockgenproof renaming fpok --> epCyril SIX2019-10-011-11/+11
| |/ / / |/| | |
* | | | Restored previous input sizes for other backendsCyril SIX2019-09-2553-60/+330
* | | | Preferring the (ifeq) approach for removing testsCyril SIX2019-09-251-0/+4
* | | | Removing NaNs from TESTS_DIFF (float precision issues..)Cyril SIX2019-09-251-0/+3
* | | | varargs2 now work correctly (bis)Cyril SIX2019-09-252-3/+15
* | | | Stub for builtins-mppa_k1c.cCyril SIX2019-09-251-0/+72
generated by cgit (git 2.34.1) at 2024-07-12 06:32:19 +0000