summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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: Update barrier definitionsBrian Campbell
2019-07-31Coq: tweak Hoare proofs a littleBrian Campbell
2019-07-31Coq: reasoning for until loopsBrian Campbell
2019-07-31Fix failing SMT testAlasdair Armstrong
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-31Remove redundant ifdef and run SMT tests by defaultAlasdair Armstrong
2019-07-31Change platform_barrier so it doesn't care about it's argument typeAlasdair Armstrong
2019-07-29Coq: add state monad version of while/until loops and lifting resultsBrian Campbell
2019-07-29Add type check after descattering to keep type environments up to dateBrian Campbell
2019-07-25Some documentation of mappings and string matchingJon French
2019-07-25Update Coq barrier definitionBrian Campbell
2019-07-25Basic port of proof machinery to CoqBrian 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-18Update aarch64_small to build with new barriersAlasdair Armstrong
2019-07-18Support DMB/DSB domainsShaked Flur
2019-07-17Add another test caseAlasdair Armstrong
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-15Add a fast path to speed up platform_read_ram: use fast_read_ram if read is 8...Robert Norton
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-04Add coq builtin for concat_str (copied from mips prelude).Robert Norton
2019-07-04Bump opam version.Robert Norton
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-27Coq: less constrained version of slice for ARM modelBrian Campbell
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-24Rules and supporting files for building aarch64_small monomorphised IsabelleBrian Campbell
2019-06-21Coq: even more robust handling of unknown goalsBrian Campbell
2019-06-21Coq: better handling of unknown constraintsBrian Campbell
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 18:42:42 +0000