summaryrefslogtreecommitdiff
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-07Subdivide README models list into REMS and external, as per suggestionAlasdair
2019-02-07Merge pull request #31 from thoughtpolice/patch-2Alasdair Armstrong
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-06README: add a link to my RISC-V implementationAustin Seipp
2019-02-06Add typechecking test from MarkAlasdair Armstrong
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-01Add test cases for integer synonymsAlasdair
2019-02-01Expand integer synonymsAlasdair Armstrong
2019-02-01Add tracing instrumention for SMTAlasdair Armstrong
2019-02-01Use same license as Sail for emacs modeAlasdair Armstrong
2019-02-01Merge pull request #29 from thoughtpolice/patch-1Alasdair Armstrong
2019-02-01Tweak HOL LEM_DIR to match riscv makefileBrian Campbell
2019-02-01Make hol libraries use opam Lem library by defaultBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:24:02 +0000