aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/lib
Commit message (Expand)AuthorAgeFilesLines
* simplifying the translation, external calls + cfi_step on builtinsSylvain Boulmé2020-04-152-196/+127
* Adjust comment to reflect progress on cfi_stepJustus Fasse2020-04-121-24/+0
* Add exec_MBjumptable to PseudoAsmblock.cfi_stepJustus Fasse2020-04-122-1/+26
* Add exec_MBcond_false to PseudoAsmblock.cfi_stepJustus Fasse2020-04-122-1/+11
* Add exec_MBcond_true to PseudoAsmblock.cfi_stepJustus Fasse2020-04-122-4/+24
* Add exec_MBtailcall to PseudoAsmblock.cfi_stepJustus Fasse2020-04-102-11/+16
* exit_step_simulation: finish MBgoto caseJustus Fasse2020-04-081-1/+3
* Merge branch 'PseudoAsmblock' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/C...Justus Fasse2020-04-061-12/+6
|\
| * with a little help of [your] friend[].Sylvain Boulmé2020-04-061-12/+6
* | exit_step_simulation: finish MBcall caseJustus Fasse2020-04-061-4/+5
|/
* Progress on match_states of exit_step_simulationJustus Fasse2020-04-031-4/+22
* Modest progress in exit_step_simulationJustus Fasse2020-03-301-1/+40
* Adjust basic_step_simulation proofJustus Fasse2020-03-271-9/+6
* easy case of exit_step_simulationSylvain Boulmé2020-03-231-0/+6
* suggestion of exit_step_simulation lemmaSylvain Boulmé2020-03-231-29/+31
* Stuck on next step of `inst_step_simulation`Justus Fasse2020-03-191-3/+23
* Finish proof for basic_step_simulationJustus Fasse2020-03-121-8/+29
* Continuation of basic_step_simulationJustus Fasse2020-03-121-1/+38
* Live proving demonstration by Sylvain.Justus Fasse2020-03-121-1/+55
* fix copy-paste error from PseudoAsmproofSylvain Boulmé2020-03-111-1/+1
* move PseudoAsmblock proof in a separate fileSylvain Boulmé2020-03-112-323/+791
* starting the PseudoAsmblock proofSylvain Boulmé2020-03-091-7/+102
* Merge branch 'mppa-work' into PseudoAsmblockSylvain Boulmé2020-03-091-4/+4
|\
| * removing some coqc 8.10 warningsSylvain Boulmé2020-03-091-4/+4
* | start PseudoAsmblockSylvain Boulmé2020-03-092-0/+549
|/
* removing warnings on hints in coreSylvain Boulmé2020-03-073-15/+15
* Moving Asmblockgenproof0 to mppa_k1c/lib/Cyril SIX2020-02-101-0/+967
* fix Focus -> { ... }David Monniaux2019-09-201-2/+2
* Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-201-3/+3
|\
| * Compatibility fix for Coq 8.7.1Cyril SIX2019-09-131-3/+3
* | more on notrapDavid Monniaux2019-09-053-4/+19
|/
* Englishification of commentsCyril SIX2019-09-032-11/+6
* move Asmblockgenproof0 from lib to mppa_k1c/Sylvain Boulmé2019-05-211-1134/+0
* move Machblock*.v into mppa_k1c/libSylvain Boulmé2019-05-213-0/+1368
* Merge remote-tracking branch 'machblock/mppa_k1c' into mppa-workCyril SIX2019-05-202-15/+52
|\
| * extract Machgen.trans_code stuff from AsmgenproofSylvain Boulmé2019-04-071-15/+1
| * squelette de preuve pour Machblockgenproof.vSylvain Boulmé2019-02-221-0/+51
* | generalize bblock_equiv into bblock_simuSylvain Boulmé2019-05-071-5/+4
* | simplification semantique+preuve des load_q+load_oSylvain Boulmé2019-05-061-4/+2
* | big proofs for so / loDavid Monniaux2019-05-041-0/+18
* | begin add PlqDavid Monniaux2019-05-031-0/+7
* | rm OfslowDavid Monniaux2019-05-031-1/+1
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-peepholeDavid Monniaux2019-05-031-2/+2
|\ \
| * | rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)David Monniaux2019-05-031-2/+2
* | | getting stuck need to move offsetsDavid Monniaux2019-05-031-0/+7
|/ /
* | it compilesDavid Monniaux2019-05-011-0/+1
* | begin load.xsDavid Monniaux2019-05-011-0/+1
* | Merge remote-tracking branch 'origin/mppa-refactor-reviewed' into mppa-refactorCyril SIX2019-04-081-1/+1
|\ \
| * | relecture sylvainSylvain Boulmé2019-04-051-1/+1
* | | #91 Removed completely the duplicated semantics in AsmblockCyril SIX2019-04-051-5/+15
|/ /
generated by cgit (git 2.34.1) at 2024-07-14 06:20:20 +0000