aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)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
|