summaryrefslogtreecommitdiff
path: root/src/sail.ml
AgeCommit message (Expand)Author
2018-01-15Refactored and improved ocaml interpreterAlasdair Armstrong
2018-01-12Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-12Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-12OCaml interactive mode can now run full aarch64 examples, and ocaml test cases.Alasdair Armstrong
2018-01-11Ocaml semantics can now run aarch64 hello world example using octapodAlasdair Armstrong
2018-01-10Add an all_split_errors optionBrian Campbell
2018-01-09Add some optional experimental rewrites to help with monomorphisationBrian Campbell
2018-01-05Moved parser, lexer and pretty printer to correct locations.Alasdair Armstrong
2018-01-05Removed legacy parser/lexer and pretty printerAlasdair Armstrong
2018-01-03Lots of experimental changes on this branchAlasdair Armstrong
2017-12-18Clean up last commitBrian Campbell
2017-12-18Handle multiple -lem_lib optionsBrian Campbell
2017-12-14Make sequential and mwords global variables in Lem pretty-printerThomas Bauereiss
2017-12-11Prototype interactive mode for sail.Alasdair Armstrong
2017-12-05Update license headers for Sail sourceAlasdair Armstrong
2017-11-30Improvements to enable parsing and checking intermediate rewritingAlasdair Armstrong
2017-11-14Automatic analysis for monomorphisationBrian Campbell
2017-11-10Fixed some tricky typechecking bugsAlasdair Armstrong
2017-11-03Fix a bug where sail would throw an exception with empty file listAlasdair Armstrong
2017-10-26Updated ocaml backend so tracing instrumentation is optional.Alasdair Armstrong
2017-10-23Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-19Rewrite undefined values, add type annotations to early returnsThomas Bauereiss
2017-10-18Merge branch 'experiments' of Peter_Sewell/sail into mono-experimentsBrian Campbell
2017-10-06Various improvements to menhir parser, and performance improvments for Z3 callsAlasdair Armstrong
2017-10-04Merge branch 'cleanup' into experimentsAlasdair Armstrong
2017-09-27Fixed command line flag namingAlasdair Armstrong
2017-09-21Cleaning up the AST and removing redundant and/or unused nodesAlasdair Armstrong
2017-09-18Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-09-07Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ex...Alasdair Armstrong
2017-09-04Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into mono-exper...Brian Campbell
2017-09-02Add command line flags to toggle sequential monad and native machine wordsThomas Bauereiss
2017-08-30Ocaml backend can now run ocamlbuild automatically to build ocamlAlasdair Armstrong
2017-08-29More work on ocaml backend.Alasdair Armstrong
2017-08-28Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into mono-exper...Brian Campbell
2017-08-24More work on undefined elimination pass.Alasdair Armstrong
2017-08-23Started work on an undefined literal removal pass for the ocamlAlasdair Armstrong
2017-08-23Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-08-22Add option to dump monomorphised ast before (re-)typecheckingBrian Campbell
2017-08-21More work on quantifier elimination passAlasdair Armstrong
2017-08-21Modified sizeof rewriting pass so it can correctly deal with existentials.Alasdair Armstrong
2017-08-17Work on E_constraint removal pass and diagnosing bugs in E_sizeof removal passAlasdair Armstrong
2017-08-10Merge remote-tracking branch 'origin/sail_new_tc' into experimentsAlasdair Armstrong
2017-08-08Add infrastructure to play with new menhir parsers.Alasdair Armstrong
2017-08-02Add debugging option to dump AST after rewriting stepsThomas Bauereiss
2017-07-27Parameterise convert_ast by the bitvector orderAlasdair Armstrong
2017-07-25Improved l-expressionsAlasdair Armstrong
2017-07-24Separate monomorphisation from top-level type checkingBrian Campbell
2017-07-24Remove monomorphisation for old type checkerBrian Campbell
2017-07-21Everything moved to new typecheckerAlasdair Armstrong
2017-07-21Switch to new typechecker (almost)Thomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 09:43:57 +0000