summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2019-08-20add -coq_alt_modules option to override the default imported modulespes20
2019-08-14Add a mono rewrite for (ones(n) @ zeros(m))Thomas Bauereiss
2019-08-14Inline reg_deref in Lem outputThomas Bauereiss
2019-08-14Use bitvector type in mono rewritesThomas Bauereiss
2019-08-13Coq: fix non-exhaustive pattern match failure in riscv duopodBrian Campbell
2019-08-08Fix machine words againAlasdair Armstrong
2019-08-08Update machine wordsAlasdair Armstrong
2019-08-08Fix bitvectorToFromInterpAlasdair Armstrong
2019-08-08Use bitToFromInterp in bitvectorToFromInterpAlasdair Armstrong
2019-08-08Add same to bitlist representationAlasdair Armstrong
2019-08-08Add bitvectorToFromInterpAlasdair Armstrong
2019-08-05Print effect sets in alphabetical orderAlasdair Armstrong
2019-08-05Remove escape/pure effect restriction for mappingAlasdair Armstrong
2019-08-02Fix all warnings (except for two lem warnings)Alasdair Armstrong
2019-08-02Fix up some edge cases with the bitvector/polyvector splitBrian Campbell
2019-08-01Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-08-01Merge remote-tracking branch 'origin/rv_duopod_fix' into sail2Alasdair Armstrong
2019-07-31Coq: reasoning for until loopsBrian Campbell
2019-07-31Revert "Need to separate out the 0.10 lem library from upcoming 0.11"Alasdair Armstrong
2019-07-31Merge branch 'sail2' into union_barrierAlasdair Armstrong
2019-07-31Updates to function unfolding to support scattered definitionsAlasdair Armstrong
2019-07-29Add type check after descattering to keep type environments up to dateBrian Campbell
2019-07-18Need to separate out the 0.10 lem library from upcoming 0.11Alasdair Armstrong
2019-07-18Add a option to check for a feature symbolAlasdair Armstrong
2019-07-18Add a feature flag for barrier type changeAlasdair Armstrong
2019-07-18Support DMB/DSB domainsShaked Flur
2019-07-16Fix all remaining tests for this branchAlasdair
2019-07-16Get monomorphisation tests working with separate bitvectorsAlasdair Armstrong
2019-07-16Merge remote-tracking branch 'origin/sail2' into separate_bvAlasdair Armstrong
2019-07-11Make sure we do constant-fold primitives howeverAlasdair Armstrong
2019-07-11Make sure constant folding won't fold external definitions that also have sai...Alasdair Armstrong
2019-07-03Consider references in topological sortingThomas Bauereiss
2019-06-30Fix bug with toplevel pattern in RISC-V duopodAlasdair
2019-06-28Monomorphisation: add some alternative names for ones and zero_extend as used...Robert Norton
2019-06-28ToFromInterp backend: always wrap typ arg values in a function, fixes option ...Jon French
2019-06-28Add a warning for potentially unsafe castsAlasdair
2019-06-27SMT: Add a reverse endianness function and fix some bugsAlasdair Armstrong
2019-06-26Fix: Make sure to consider NC_app when checking constraints are identicalAlasdair Armstrong
2019-06-26Make sure we take constraint synonyms into account when checking if types are...Alasdair Armstrong
2019-06-25SMT: Add another case to appendAlasdair Armstrong
2019-06-21Coq: add missing property derivation casts for effectful expressionsBrian Campbell
2019-06-21Coq: be more careful when dealing with wildcard argument patternsBrian Campbell
2019-06-20Coq: avoid more unnecessary uses of pattern bindersBrian Campbell
2019-06-20Coq: handle wildcard binders of bools properlyBrian Campbell
2019-06-20Add additional case to append for Sail -> SMTAlasdair Armstrong
2019-06-20Add more cases to signed for Sail SMTAlasdair Armstrong
2019-06-20Handle more uses of mutable variables during monomorphisation cast insertionBrian Campbell
2019-06-19Make C emulator exit with failure for uncaught exception. Make special case f...Robert Norton
2019-06-19Make default ocaml main exit with non-zero exit code in case of uncaught exce...Robert Norton
2019-06-19Fix buggy ocaml implementation of count_leading_zeros and also make tail recu...Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:22:23 +0000