aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* fix for jump tablesv3.5_k1c_1.0David Monniaux2019-03-302-18/+19
* FIXME: Jumptables have linking issues.David Monniaux2019-03-294-0/+1245
* Merge branch 'mppa_k1c' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2019-03-291-8/+8
|\
| * Merge branch 'mppa-mul' into mppa_k0cDavid Monniaux2019-03-2921-1082/+1916
| |\
| * | rm rules that conflictDavid Monniaux2019-03-291-8/+8
* | | Merge remote-tracking branch 'origin/mppa_k1c' into mppa-mulDavid Monniaux2019-03-2912-72/+235
|\| |
| * | use C99 modeDavid Monniaux2019-03-291-1/+1
| * | Merge remote-tracking branch 'origin/mppa-jumptable' into mppa-jumptableCyril SIX2019-03-291-2/+5
| |\ \
| | * | Finition de la preuve de AsmblockgenproofCyril SIX2019-03-291-2/+5
| * | | Preuve de Jumptable dans Asmblockdeps.vCyril SIX2019-03-292-1/+24
| * | | Merge remote-tracking branch 'origin/mppa_postpass' into mppa-jumptableCyril SIX2019-03-298-24/+1121
| |\ \ \ | | |/ / | |/| |
| | * | No more AdmittedCyril SIX2019-03-291-55/+102
| * | | Avancement dans la preuve du MBjumptableCyril SIX2019-03-291-1/+21
| * | | for testing with questDavid Monniaux2019-03-221-0/+24
| * | | xMerge branch 'mppa-mul' into mppa-jumptableDavid Monniaux2019-03-221-0/+3
| |\ \ \
| * | | | check that gcc and ccomp compiled k1c code return the sameDavid Monniaux2019-03-221-2/+6
| * | | | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd)David Monniaux2019-03-221-1/+1
| * | | | improved testingDavid Monniaux2019-03-221-5/+16
| * | | | uses yarpgen random generatorDavid Monniaux2019-03-221-0/+37
| * | | | some more testingDavid Monniaux2019-03-221-1/+1
| * | | | Merge branch 'mppa-mul' into mppa-jumptableDavid Monniaux2019-03-22302-6460/+51288
| |\ \ \ \
| * | | | | Jump tables now work. There is still an "Admitted" subcase in a proof.David Monniaux2019-03-223-5/+15
| * | | | | on avance sur la jumptableDavid Monniaux2019-03-222-3/+3
| * | | | | jumptable avanceDavid Monniaux2019-03-221-1/+8
| * | | | | Fixed proof of Asmblockdeps wrt PjumptableCyril SIX2019-03-221-25/+28
| * | | | | begin jumptables (does not work)David Monniaux2019-03-215-8/+57
* | | | | | missing config.hDavid Monniaux2019-03-291-0/+3
* | | | | | Makefile for picosatDavid Monniaux2019-03-293-62/+0
| |_|_|_|/ |/| | | |
* | | | | ocaml benchmarkDavid Monniaux2019-03-283-8/+22
* | | | | MakefileDavid Monniaux2019-03-285-1025/+35
* | | | | NDEBUGDavid Monniaux2019-03-281-0/+6
* | | | | some more inlineDavid Monniaux2019-03-282-12/+13
* | | | | add some INLINE markersDavid Monniaux2019-03-281-36/+38
* | | | | picosat now uses the same Makefile system as the restDavid Monniaux2019-03-283-3/+49
* | | | | merge proof of VLIWDavid Monniaux2019-03-288-24/+1074
|\ \ \ \ \ | | |_|_|/ | |/| | |
| * | | | Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpassDavid Monniaux2019-03-2810-75/+1072
| |\ \ \ \
| | * \ \ \ Merge branch 'mppa_vliw_essai_sylvain' of gricad-gitlab.univ-grenoble-alpes.f...Sylvain Boulmé2019-03-272-67/+80
| | |\ \ \ \
| | | * | | | Proof of the entire forward simulation (still stuck to do + permutations)Cyril SIX2019-03-271-3/+10
| | | * | | | Preuve du forward_simu du parexec_wio_bblock_auxCyril SIX2019-03-272-60/+70
| | * | | | | dealing with permutationsSylvain Boulmé2019-03-272-29/+100
| | |/ / / /
| | * | | | Avancement dans Asmblockdeps.vCyril SIX2019-03-272-91/+113
| | * | | | 1 coup de pouce !Sylvain Boulmé2019-03-261-9/+29
| | * | | | Un peu d'avancementCyril SIX2019-03-262-4/+287
| | * | | | slight simplificationSylvain Boulmé2019-03-231-5/+4
| | * | | | Avancement dans la preuve des bundlesCyril SIX2019-03-221-3/+51
| | * | | | fix for Coq.8.8 ??Sylvain Boulmé2019-03-222-4/+3
| | * | | | Décomposition de la preuve en une forward_simu_par_stuck et une forward_simu...Cyril SIX2019-03-222-1/+72
| | * | | | simplification of the proofSylvain Boulmé2019-03-212-29/+70
| | * | | | yet another step backwardSylvain Boulmé2019-03-201-18/+39
| | * | | | one step further...Sylvain Boulmé2019-03-201-6/+28
generated by cgit (git 2.34.1) at 2024-05-20 07:19:55 +0000