summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2019-02-08Updates for asl_parserAlasdair Armstrong
2019-02-08Rewrite type definitions in rewrite_nexp_idsThomas Bauereiss
2019-02-08Remove dead code from type-checkerAlasdair
2019-02-07Replace equality check for declared effects by subset checkThomas Bauereiss
2019-02-07Monomorphisation tweaks for v8.5Thomas Bauereiss
2019-02-07Add a symbol for new implicit arguments for backwards compatabilityAlasdair Armstrong
2019-02-07Fix implicits in v8.2 public ARM specAlasdair Armstrong
2019-02-06Emacs mode understands relationships between Sail filesAlasdair
2019-02-06Improve emacs modeAlasdair Armstrong
2019-02-06Fix some testsAlasdair Armstrong
2019-02-06Make sure type synonym errors have correct location infoAlasdair Armstrong
2019-02-06Remove all sizeof rewriting from C compilationAlasdair
2019-02-05Simpler implicit argumentsAlasdair Armstrong
2019-02-05Ensure Lem output doesn't fail if there's a termination measure presentBrian Campbell
2019-02-05Use more general types for lexps in the internal lets rewriting passBrian Campbell
2019-02-05The alpha equivalence check should keep tyvars that only appear in constraintsBrian Campbell
2019-02-05Handle a few more cases in mono rewritesThomas Bauereiss
2019-02-04Fix some warningsAlasdair Armstrong
2019-02-04Add dec_str builtin to lemAlasdair Armstrong
2019-02-04Test lem output by running end-to-end tests using ocaml via lemAlasdair Armstrong
2019-02-04Fix behavior for fallthrough cases in catch blocksAlasdair Armstrong
2019-02-03Merge branch 'sail2' into rmem_interpreterJon French
2019-02-02Avoid unification on ambiguous return typesAlasdair
2019-02-02Monomorphisation tests all pass so add them to standard regression testsAlasdair
2019-02-02Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-02-01Fix missing typedef cases in OCaml outputAlasdair
2019-02-01Expand integer synonymsAlasdair Armstrong
2019-02-01Add tracing instrumention for SMTAlasdair Armstrong
2019-01-31Fix an unnecessary cast insertion on assignmentsBrian Campbell
2019-01-31Turn on cast insertion for -lem_mwords and revert b826df25Brian Campbell
2019-01-31Drop type annotations in top-level nexp rewriting in favour of valspecsBrian Campbell
2019-01-31Make cast insertion handle more complex nexps and pushing casts into blocksBrian Campbell
2019-01-31Merge branch 'monads' into asl_flow2Thomas Bauereiss
2019-01-31Further restrict attention to Int kidsThomas Bauereiss
2019-01-31Monomorphisation: improve cast insertion and nexp rewriting on variantsBrian Campbell
2019-01-31Add missing cases to constraint comparisonBrian Campbell
2019-01-31Support case splitting on variables as well as sizeof in cast introductionBrian Campbell
2019-01-30Cache compilation results to improve build times for repeated buildsAlasdair
2019-01-29Fixes for full v8.5Alasdair Armstrong
2019-01-29Add an option to crudely slice a function out of a Sail modelBrian Campbell
2019-01-29Monomorphisation: add missing tyvar substitution during constrant propagationBrian Campbell
2019-01-29Add a few more type annotations after mono rewritesThomas Bauereiss
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-29Improve generation of initial register stateThomas Bauereiss
2019-01-29Monomorphisation: restrict our attention to Int kidsBrian Campbell
2019-01-28Lem: Be more careful about nexps occurring in the function signatureThomas Bauereiss
2019-01-25Monomorphisation: update a built-in nameBrian Campbell
2019-01-25Fix solution finding using SMT by looking for the right variableBrian Campbell
2019-01-25Coq: add enough to generate some output for arm-v8.5-aBrian Campbell
2019-01-24Start supporting informative bool types in Coq backendBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 01:29:29 +0000