summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2019-02-12Add a CHANGELOG fileAlasdair Armstrong
2019-02-12Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair Armstrong
2019-02-12Improvements for emacs modeAlasdair Armstrong
2019-02-11Add an additional test caseAlasdair
2019-02-11Expand type synonyms for E_constraint and E_sizeofAlasdair
2019-02-11Add tests for implicit argumentsAlasdair Armstrong
2019-02-11Get the order of overrides correct during topsortBrian Campbell
2019-02-08Cleanup src MakefileAlasdair
2019-02-08Slightly tweak the help message.Prashanth Mundkur
2019-02-08Add parameterization support for bitfields.Prashanth Mundkur
2019-02-08Add missing functions to HOL monad wrapperThomas Bauereiss
2019-02-08Resurrect Sail output option (with new name: -output_sail)Brian Campbell
2019-02-08Prevent top_sort throwing away overloads (and other multiple definitions)Brian Campbell
2019-02-08Allow internal AST nodes in input when -dmagic_hash is onBrian Campbell
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:40:18 +0000