aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Expand)AuthorAgeFilesLines
* Finish DeadBlocksproofYann Herklotz2022-07-013-101/+158
* Merge remote-tracking branch 'origin/dev/scheduling' into dev/schedulingYann Herklotz2022-07-012-75/+466
|\
| * Working on extending ifconversion proofYann Herklotz2022-06-302-0/+20
| * Remove useless commentsYann Herklotz2022-06-301-9/+0
| * Finish if-conversion proofYann Herklotz2022-06-301-1/+148
| * Nearly finished if-conversion proofYann Herklotz2022-06-302-65/+298
* | Add dead code elimination proof mostlyYann Herklotz2022-07-011-0/+1052
|/
* Update proofYann Herklotz2022-06-302-37/+102
* Work on if-conversion proofYann Herklotz2022-06-283-47/+282
* Merge remote-tracking branch 'origin/dev/scheduling' into dev/schedulingYann Herklotz2022-06-282-21/+92
|\
| * Merge remote-tracking branch 'origin/dev/scheduling' into dev/schedulingYann Herklotz2022-06-286-18/+22
| |\
| * | Add if-conversion specYann Herklotz2022-06-282-21/+92
* | | Update if-conversion functionYann Herklotz2022-06-282-3/+10
| |/ |/|
* | Update build files for documentationYann Herklotz2022-06-241-3/+3
* | Update documentation for GibleYann Herklotz2022-06-245-15/+19
|/
* Work on the if-conversion proofYann Herklotz2022-06-092-32/+49
* Rearrange definitions and create IfConversion templateYann Herklotz2022-06-066-105/+301
* Finish CondElim proof and fix Gible semanticsYann Herklotz2022-06-063-134/+246
* Fix many more lemmasYann Herklotz2022-06-054-109/+329
* Remove inv H1 from condelim proofYann Herklotz2022-06-051-3/+3
* Add condelim proofYann Herklotz2022-06-051-85/+169
* work on condelimproofYann Herklotz2022-06-041-66/+72
* Add to condelim proofYann Herklotz2022-06-041-2/+111
* Working towards ElimCond proofYann Herklotz2022-06-032-34/+87
* Work on CondElim proofYann Herklotz2022-06-036-24/+111
* Do not remove dependencies from control-flowYann Herklotz2022-05-311-1/+6
* Place both case statements into the same always blockYann Herklotz2022-05-311-4/+5
* Abstract useful function into Predicate.vYann Herklotz2022-05-311-0/+7
* Fix hardware generationYann Herklotz2022-05-311-59/+79
* Fix GibleSeqgenproof with new semanticsYann Herklotz2022-05-312-54/+70
* Fix update function for control-flowYann Herklotz2022-05-311-1/+12
* Update the Gible semantics with correct terminationYann Herklotz2022-05-311-9/+10
* Add new translations to top-levelYann Herklotz2022-05-311-1/+7
* Simplify if-conversion passYann Herklotz2022-05-311-30/+80
* Add new translation passes for if-conversionYann Herklotz2022-05-313-0/+337
* Fix code generation in partitioning and schedulingYann Herklotz2022-05-274-9/+54
* Rewrite a lot fixing scheduling of GibleYann Herklotz2022-05-2723-646/+366
* Add new block generation for GibleYann Herklotz2022-05-266-457/+298
* Translate the base languagesYann Herklotz2022-05-257-437/+431
* Famous proven but not tested has been fixedYann Herklotz2022-05-123-13/+13
* Completely finish RTLBlockgenproofYann Herklotz2022-05-122-24/+171
* Remove imm_succ from match_blockYann Herklotz2022-05-121-100/+27
* Add rest of the proofsYann Herklotz2022-05-121-12/+272
* Up to Icall is now provenYann Herklotz2022-05-122-86/+382
* Try to expand the definition of match_codeYann Herklotz2022-05-121-23/+35
* Finish Inop proof for basic block generationYann Herklotz2022-05-111-12/+24
* Add new definitions of match_codeYann Herklotz2022-05-111-8/+13
* Change the specification of the RTLBlockgenproofYann Herklotz2022-05-091-31/+45
* Try to work on refining the match_states predicateYann Herklotz2022-05-061-9/+22
* Try out a new match_code predicateYann Herklotz2022-04-251-13/+30
generated by cgit (git 2.34.1) at 2024-07-02 22:09:15 +0000