aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| | * | | | | 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 VLIW proofsDavid Monniaux2019-03-2813-1551/+1113
|\| | | | |
| * | | | | 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
| | | * | | | premier decoupageSylvain Boulmé2019-03-201-2/+56
| | | * | | | Integrating Asmvliw.v in the proof chainCyril SIX2019-03-204-17/+30
| | | * | | | Idée de preuve VLIWCyril SIX2019-03-181-2/+21
| | | * | | | fix the step_internal of AsmvliwSylvain Boulmé2019-03-141-19/+23
| | | * | | | definition of VLIW semanticsSylvain Boulmé2019-03-143-14/+342
| * | | | | | some more ternaryDavid Monniaux2019-03-241-6/+6
| * | | | | | experiments with ternary operatorDavid Monniaux2019-03-241-1/+6
| * | | | | | experiments with ternaryDavid Monniaux2019-03-244-1526/+36
| * | | | | | another ternary implementationDavid Monniaux2019-03-241-1/+7
* | | | | | | don't penalize x86 CompCertDavid Monniaux2019-03-271-1/+1
* | | | | | | put both compilers in their best moodDavid Monniaux2019-03-271-5/+18
* | | | | | | switch off ternary if not CompCertDavid Monniaux2019-03-271-14/+4
* | | | | | | improvements on cmoved etc.David Monniaux2019-03-273-97/+18
* | | | | | | work on ternaryDavid Monniaux2019-03-272-8/+21
* | | | | | | hand optimizedDavid Monniaux2019-03-272-0/+3271
* | | | | | | match some 'and'David Monniaux2019-03-274-14/+50
* | | | | | | essai du cmoveDavid Monniaux2019-03-273-3/+30
* | | | | | | selectl generationDavid Monniaux2019-03-266-14/+205
* | | | | | | ternary transfoDavid Monniaux2019-03-262-1/+37
* | | | | | | ternary unsignedDavid Monniaux2019-03-263-0/+54
* | | | | | | rm cruftDavid Monniaux2019-03-262-167/+9
* | | | | | | cmoved worksDavid Monniaux2019-03-261-4/+5
generated by cgit (git 2.34.1) at 2024-07-11 22:33:43 +0000