aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into dev/michalisdev/michalisYann Herklotz2021-10-1843-811/+4239
|\
| * [sched] Fix passes with new predicatesYann Herklotz2021-10-142-1/+3
| * [sched] Add combination of equivalent expressionsYann Herklotz2021-10-141-10/+40
| * [sched] Add true and false predicates to typeYann Herklotz2021-10-141-1/+23
| * [sched] Finish det proofs of basic Abstr semanticsYann Herklotz2021-10-131-27/+44
| * [sched] Add more proof to sem_pred_detYann Herklotz2021-10-132-1/+6
| * [sched] Add proofs of sem_pred_detYann Herklotz2021-10-131-8/+44
| * [sched] Add start to proof of sem_value_detYann Herklotz2021-10-121-0/+12
| * [sched] Remove unnecessary importsYann Herklotz2021-10-121-11/+0
| * [sched] Add more lemmas into HashTreeYann Herklotz2021-10-122-10/+37
| * [sched] Update Abstr.v to use HashTreeYann Herklotz2021-10-121-29/+97
| * [sched] Add HashTree.v for hashing arbitrary valuesYann Herklotz2021-10-121-0/+413
| * Add div benchmarks to .gitignoreYann Herklotz2021-10-121-0/+28
| * Update .gitignore againYann Herklotz2021-10-121-27/+27
| * Add updated .gitignore for benchmarksYann Herklotz2021-10-121-0/+40
| * Merge branch 'dev/scheduling' of git.ymhg.org:vericert into dev/schedulingYann Herklotz2021-10-1212-76/+94
| |\
| | * Fix some of the testing in MakefileYann Herklotz2021-10-091-3/+3
| | * Update the changelogYann Herklotz2021-10-091-3/+7
| | * Fix warnings for Coq 8.13.2Yann Herklotz2021-10-0910-70/+84
| * | [sched] Small changes to definitionsYann Herklotz2021-10-121-5/+5
| |/
| * End section in Abstr.vYann Herklotz2021-10-081-0/+2
| * Add abstract intermediate language to RTLPargenYann Herklotz2021-10-081-17/+49
| * Remove warnings of attributesYann Herklotz2021-10-083-126/+126
| * Make HTLgenproof passYann Herklotz2021-10-081-1/+1
| * Add proof of beq_check_correctnessYann Herklotz2021-10-081-57/+120
| * Fix running of tests using a MakefileYann Herklotz2021-10-082-1/+36
| * Add scheduling by default to benchmark executionYann Herklotz2021-10-071-1/+1
| * Fix naming and remove warningsYann Herklotz2021-10-072-10/+10
| * RTLPargen now uses Abstr as symbolic execution targetYann Herklotz2021-10-071-705/+1
| * Update functional units to be more generalYann Herklotz2021-10-071-14/+62
| * Add Abstr intermediate languageYann Herklotz2021-10-071-0/+749
| * [test] Fix testing from MakefileYann Herklotz2021-10-011-0/+2
| * [scheduling] Fix connected components of DFGYann Herklotz2021-10-011-6/+7
| * Merge branch 'master' into dev/schedulingYann Herklotz2021-10-014-13/+20
| |\
| | * Add menhirLib as an explicit dependencyYann Herklotz2021-10-011-0/+1
| | * Update README with checkout instructionsYann Herklotz2021-10-011-10/+12
| | * Merge branch 'release/v1.2.2'Yann Herklotz2021-10-013-3/+7
| | |\
| | | * Fix citation file and READMEv1.2.2stableYann Herklotz2021-10-012-3/+2
| | | * Update Changelog with 1.2.2 releaseYann Herklotz2021-10-011-0/+5
| | * | Merge branch 'develop'Yann Herklotz2021-10-0121-280/+2735
| | |\ \ | | | |/ | | |/|
| | * | Merge remote-tracking branch 'origin/master'Yann Herklotz2021-09-291-3/+3
| | |\ \
| | | * | Update README on the status of VericertYann Herklotz2021-09-271-2/+2
| | | * | Add empty titleYann Herklotz2021-09-272-0/+2
| | * | | Update docsYann Herklotz2021-09-291-0/+0
| | * | | Export without titleYann Herklotz2021-09-271-0/+2
| | |/ /
| * | / Improve pretty-printing and add undirected graphYann Herklotz2021-10-012-7/+23
| | |/ | |/|
| * | Fix equivalence checkingYann Herklotz2021-10-012-5/+2
| * | Add printers for expressions and RTLParYann Herklotz2021-10-012-0/+114
| * | Fix compilation of new intermediate languagesYann Herklotz2021-10-016-12/+21
| * | Improve equivalence checking using SATYann Herklotz2021-10-011-15/+22