aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/abstractbb
Commit message (Expand)AuthorAgeFilesLines
* generalize bblock_equiv into bblock_simu (abstract_bb)Sylvain Boulmé2019-05-075-51/+42
* update from Impure LibrarySylvain Boulmé2019-04-111-20/+22
* refactor for #92Sylvain Boulmé2019-04-112-5/+31
* moving iandb from ImpCore to ImpPreludeSylvain Boulmé2019-04-082-23/+18
* Impure: improved iandb + struct_eqSylvain Boulmé2019-04-012-3/+11
* renommage abstractbb: Name -> PRegSylvain Boulmé2019-04-014-7/+7
* renommages abstract_bbSylvain Boulmé2019-04-014-132/+132
* minor simplSylvain Boulmé2019-04-011-8/+14
* delete useless DepExample* filesSylvain Boulmé2019-04-014-1051/+0
* Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpassDavid Monniaux2019-03-281-0/+18
|\
| * dealing with permutationsSylvain Boulmé2019-03-271-0/+18
* | remove a FAILWITH that forbids some debugging information to be printedSylvain Boulmé2019-03-191-3/+3
|/
* Fix for CompCert 3.5Cyril SIX2019-03-131-0/+1
* quick fix of equalities issuesSylvain Boulmé2019-03-051-0/+4
* fix extraction of ImpConfigSylvain Boulmé2019-03-051-2/+5
* compilation of ImpIOOraclesSylvain Boulmé2019-03-052-4/+8
* remove cumbersome dependency on genv in bblock_eq_testSylvain Boulmé2019-03-053-27/+27
* (Unsafe) coercion of ??bool into boolSylvain Boulmé2019-03-021-2/+2
* [BROKEN] trying to generalize Sylvain's abstract bb to include a genv.Cyril SIX2019-02-207-87/+133
* Added AbstractBasicBlock files to the Coq build processCyril SIX2019-02-1325-0/+4692
generated by cgit (git 2.34.1) at 2024-07-02 10:10:04 +0000