summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-01-12Support constant propagation on casts in monomorphisationBrian Campbell
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-10Fix control dependencies in monomorphisation analysisBrian Campbell
2018-01-09More monomorphisation rewrites for aarch64Brian Campbell
2018-01-09Tidy up monomorphisation interfaceBrian Campbell
2018-01-09Proper location for no set constraint errorsBrian Campbell
2018-01-09Move reordering in alpha_equivalent before relabelling to giveBrian Campbell
2018-01-09Add some optional experimental rewrites to help with monomorphisationBrian Campbell
2018-01-08Improved fix for alpha-equivalence re-ordering issueAlasdair Armstrong
2018-01-08Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ex...Alasdair Armstrong
2018-01-08Potential fix for bug where different quantifer order in existentials will br...Alasdair Armstrong
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-05Fix duplicate definitions created by mergeAlasdair Armstrong
2018-01-05Merge remote-tracking branch 'origin/interactive' into vectorAlasdair Armstrong
2018-01-05Added sail_lib fileAlasdair Armstrong
2018-01-05Added bitfield syntax to replicate register bits typeAlasdair Armstrong
2018-01-04Additional tests for ocaml backendAlasdair Armstrong
2018-01-03Lots of experimental changes on this branchAlasdair Armstrong
2018-01-03Updates to interpreterAlasdair Armstrong
2018-01-02Experimenting with power specAlasdair Armstrong
2017-12-30use linksem as a packageShaked Flur
2017-12-28use ocamlfind to locate lem and zarith (missed this Makefile)Shaked Flur
2017-12-28use ocamlfind to locate lem and zarithShaked Flur
2017-12-19Support user-defined exceptions in Lem shallow embeddingThomas Bauereiss
2017-12-19Add rewriting step for numeral patternsThomas Bauereiss
2017-12-19Fix a bug in untupling function arguments for LemThomas Bauereiss
2017-12-18Clean up last commitBrian Campbell
2017-12-18Handle multiple -lem_lib optionsBrian Campbell
2017-12-16compatibility with OCaml 4.06.0;Shaked Flur
2017-12-15Experimenting with interactive modeAlasdair Armstrong
2017-12-14An experimental version of sail without bitvector start indexes.Alasdair Armstrong
2017-12-14Un-tuple function arguments when pretty-printing to LemThomas Bauereiss
2017-12-14Make sequential and mwords global variables in Lem pretty-printerThomas Bauereiss
2017-12-14Merge remote-tracking branch 'origin/experiments' into interactiveAlasdair Armstrong
2017-12-14Fix all compiler warning except in lem pretty printer and monomorphisationAlasdair Armstrong
2017-12-13Cleanup code by fixing compiler warnings, and fix ocaml compilationAlasdair Armstrong
2017-12-13Merge remote-tracking branch 'origin/master' into interactiveAlasdair Armstrong
2017-12-13Use big_nums from LemAlasdair Armstrong
2017-12-13find zarith using ocamlfind instead of using the one in ocaml-lib which is no...Shaked Flur
2017-12-12Add a few helper functions for bit listsThomas Bauereiss
2017-12-12Make mono analysis fail properly on effectful functionsBrian Campbell
2017-12-11Allow stepping through code when evaluatingAlasdair Armstrong
2017-12-11Prototype interactive mode for sail.Alasdair Armstrong
2017-12-11Remove some duplication from monomorphisation analysis failure reportsBrian Campbell
2017-12-07More OCaml test casesAlasdair Armstrong
2017-12-07Fix boolean literal constraintsAlasdair Armstrong
2017-12-07Fix regressions in OCaml outputAlasdair Armstrong
2017-12-07Support monomorphisation with set constrained integersBrian Campbell