aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblockdeps.v
Commit message (Collapse)AuthorAgeFilesLines
* Fixing issue with "destruct ... in ..." tactics with Coq 8.8Cyril SIX2020-01-091-5/+5
|
* swap load and store at disjoint offsetsDavid Monniaux2019-12-161-1/+53
|
* swap stores at disjoint offsetsDavid Monniaux2019-12-161-16/+30
|
* comment out theorem that cannot be provedDavid Monniaux2019-12-141-29/+33
|
* progress in chunksDavid Monniaux2019-12-131-45/+9
|
* some subgoal was provedDavid Monniaux2019-12-121-6/+61
|
* begin overlap proofsDavid Monniaux2019-12-111-0/+43
|
* Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-021-2/+8
|\
| * fixing a potential inconsistency from unsafe_coerceSylvain Boulmé2019-11-141-2/+8
| | | | | | | | | | Now, unsafe_coerce axioms are clearly consistent (for any interpretation of may-return monads). But, the extraction is still unsafe...
* | moving forward on K1CDavid Monniaux2019-09-071-37/+66
|/
* Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-workCyril SIX2019-09-031-0/+9
|\ | | | | | | | | | | | | Conflicts: configure mppa_k1c/Archi.v mppa_k1c/Asmexpand.ml
| * fmaDavid Monniaux2019-08-301-0/+4
| |
| * add finvw ; not yet generatedDavid Monniaux2019-08-301-0/+1
| |
| * fmin/fmax/fminf/fmaxf non bien testésDavid Monniaux2019-08-291-0/+4
| |
* | (#156) - Un peu de cleaning et de docCyril SIX2019-07-301-20/+15
| |
* | (#139) - Quelques renommagesCyril SIX2019-07-301-5/+5
|/
* (#107) Rename "forward_simu" into "bisimu"Cyril SIX2019-07-171-27/+27
|
* maj forward_simu_par_wio_bblock_aux en forward_simu_par_wioSylvain Boulmé2019-06-231-12/+10
| | | | avec une legere simplification (comme dans le papier)
* Merge branch 'mppa-work' into mppa-abstractbb-devSylvain Boulmé2019-06-081-1/+17
|\
| * added immediate cmoveDavid Monniaux2019-06-041-0/+4
| |
| * begin generating Prevsub etc. from Oxxx to PxxxDavid Monniaux2019-05-111-6/+6
| |
| * new instructions at asm levelDavid Monniaux2019-05-101-1/+13
| |
* | simpler definition of reduceSylvain Boulmé2019-05-281-4/+15
| |
* | extending bblock_simu_test with rewritingSylvain Boulmé2019-05-261-35/+28
|/
* generalize bblock_equiv into bblock_simu (abstract_bb)Sylvain Boulmé2019-05-071-22/+17
|
* generalize bblock_equiv into bblock_simuSylvain Boulmé2019-05-071-16/+16
|
* simplification semantique+preuve des load_q+load_oSylvain Boulmé2019-05-061-255/+62
|
* mergedDavid Monniaux2019-05-041-4/+3
|
* Merge branch 'mppa-peephole' of ↵David Monniaux2019-05-041-5/+2
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-peephole
| * legere simplification de preuveSylvain Boulmé2019-05-041-70/+26
| |
* | big proofs for so / loDavid Monniaux2019-05-041-3/+199
|/
* Lq finished ?David Monniaux2019-05-031-15/+16
|
* begin add PlqDavid Monniaux2019-05-031-2/+58
|
* use sq to save pairs of registersDavid Monniaux2019-05-031-3/+16
|
* ça avanceDavid Monniaux2019-05-031-0/+27
|
* Merge remote-tracking branch 'origin/mppa-work' into mppa-peepholeDavid Monniaux2019-05-031-4/+5
|\
| * rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)David Monniaux2019-05-031-4/+5
| |
* | getting stuck need to move offsetsDavid Monniaux2019-05-031-3/+8
|/
* does not yet work, arity mismatchDavid Monniaux2019-05-011-0/+1
|
* it compilesDavid Monniaux2019-05-011-0/+20
|
* begin load.xsDavid Monniaux2019-05-011-0/+20
|
* removed fake ops for int32 -> doubleDavid Monniaux2019-04-291-2/+0
|
* Srsd / SrswDavid Monniaux2019-04-291-0/+4
|
* begin add bitfield insertionDavid Monniaux2019-04-271-2/+18
|
* start of extfzl/extfslDavid Monniaux2019-04-251-0/+2
|
* progressDavid Monniaux2019-04-251-0/+1
|
* begin bitfieldsDavid Monniaux2019-04-241-0/+1
|
* more robust pattern-matching in *op_eqSylvain Boulmé2019-04-111-8/+10
|
* refactor for #92Sylvain Boulmé2019-04-111-785/+305
|
* achieve issue #89 ?Sylvain Boulmé2019-04-101-185/+47
|
generated by cgit (git 2.34.1) at 2024-07-14 11:04:34 +0000