aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * | Fix scheduler for operation chainingYann Herklotz2021-10-011-8/+22
| * | Add back scheduling to the driverYann Herklotz2021-09-302-2/+2
| * | Merge remote-tracking branch 'origin/develop' into developYann Herklotz2021-09-2913-56/+1259
| |\ \
| | * | Make all OCaml files compileYann Herklotz2021-09-292-4/+4
| | * | Revert "Remove more OCaml files to compile successfully without admits."Yann Herklotz2021-09-275-0/+1085
| | * | Add dependencies for Alectryon documentationYann Herklotz2021-09-275-9/+15
| | * | Compile HTLPargen againYann Herklotz2021-09-242-6/+5
| | * | Fix scopingYann Herklotz2021-09-241-12/+10
| | * | Add back top-level functionsYann Herklotz2021-09-241-40/+157
| * | | Export without titleYann Herklotz2021-09-271-0/+2
| |/ /
| * | RTLpargen passes compilation againYann Herklotz2021-09-222-10/+18
| * | Merge remote-tracking branch 'origin/develop' into developYann Herklotz2021-09-2290-1650/+4575
| |\ \
| | * | Fix the comparison of predicated expressionsYann Herklotz2021-09-221-138/+174
| | * | Change Inductive to recordYann Herklotz2021-09-223-18/+17
| | * | Start adding hashing to RTLPargenYann Herklotz2021-09-202-7/+51
| | * | Merge branch 'master' into developYann Herklotz2021-09-202-12/+22
| | |\|
| | | * Update the docsYann Herklotz2021-09-201-0/+0
| | | * Improve the changelogYann Herklotz2021-09-181-10/+24
| | * | Merge branch 'master' into developYann Herklotz2021-09-1887-1521/+4378
| | |\|
| * | | Add full proof of SAT conversionYann Herklotz2021-07-241-2/+22
| * | | Finish SAT proofYann Herklotz2021-07-241-3/+4
| |/ /
| * | New release information to the changelogYann Herklotz2021-07-071-0/+3
| * | Add changelog which mentions the RAM supportYann Herklotz2021-07-071-0/+1
| * | Add predicate semantics to abstractYann Herklotz2021-05-261-69/+296
| * | Add predicate semantics to RTLParYann Herklotz2021-05-261-7/+8
| * | Add predicate semantics to RTLBlockYann Herklotz2021-05-261-7/+8
| * | Fix if-conversion pass with positivesYann Herklotz2021-05-261-1/+1
| * | Change naturals to positive in predicatesYann Herklotz2021-05-262-45/+79
| * | Add very top-level proofYann Herklotz2021-05-231-0/+33
| * | Fix admitted in last theoremYann Herklotz2021-05-211-3/+8
| * | Finish top-level of proofYann Herklotz2021-05-212-22/+23
| * | Minimise the proof a bitYann Herklotz2021-05-161-18/+12
| * | Finish up step_cf_instr_correct againYann Herklotz2021-05-162-19/+43
| * | Fix the top-level proofs with new state_matchYann Herklotz2021-05-152-27/+164
| * | Finish abstract interpretationYann Herklotz2021-05-121-75/+199
| * | Fix admitted in first proof of sem. preservationYann Herklotz2021-05-101-19/+68
| * | Finish correctness of semantics wrt. RTBlockYann Herklotz2021-05-061-84/+327
| * | Add admitted proof of translations in RTLPargenYann Herklotz2021-05-031-27/+177
* | | Check: only main uses ainstack, no calls to mainMichalis Pardalos2021-10-171-20/+66
* | | Check that only main has a stacksizeMichalis Pardalos2021-10-112-12/+47
* | | Get all call and return proofs passing againMichalis Pardalos2021-10-081-4/+25
* | | Maintain that initial call does not have argumentsMichalis Pardalos2021-10-071-0/+1
* | | [WIP] Handle empty stack case for empty stack caseMichalis Pardalos2021-10-071-39/+65
* | | Clarify ireturn proofMichalis Pardalos2021-09-301-5/+5
* | | Prove match_arrs_emptyMichalis Pardalos2021-09-301-1/+19
* | | Complete alloc/free zero proofsMichalis Pardalos2021-09-301-8/+15
* | | Complete call/return proofsMichalis Pardalos2021-09-301-68/+122
* | | [WIP] Updating proof for new state matchingMichalis Pardalos2021-09-291-39/+69
* | | Update match_states. Pointers based on main's spMichalis Pardalos2021-09-291-21/+27
* | | Add assumptions about externctrl finish registersMichalis Pardalos2021-09-211-21/+131
generated by cgit (git 2.34.1) at 2024-05-14 17:46:34 +0000