summaryrefslogtreecommitdiff
path: root/src/rewrites.ml
AgeCommit message (Expand)Author
2018-01-29Add rreg effect to _reg_deref in fix_val_specs rewriteThomas Bauereiss
2018-01-29Leave pure if-conditions in place instead of pulling out let-bindingsBrian Campbell
2018-01-29Get typechecking to resolve overriding in remove numeral patterns rewriteBrian Campbell
2018-01-29Move subst to ast_util, use for guarded clauses rewriteBrian Campbell
2018-01-25Omit redundant let-bindings when rewriting (bit-)vector patternsThomas Bauereiss
2018-01-25Rewrite bitvector patterns for OCaml and C backendsThomas Bauereiss
2018-01-25Fix more type annotations in rewriterThomas Bauereiss
2018-01-24Have some simple sail programs compiling to CAlasdair Armstrong
2018-01-23Run tests for Lem shallow embeddingThomas Bauereiss
2018-01-23Added additional tests, and fixed ocaml build of ARM testsAlasdair Armstrong
2018-01-22Update Lem shallow embedding to Sail2Thomas Bauereiss
2018-01-18Clean up command line options slightlyAlasdair Armstrong
2018-01-18Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-18Modified unification so Type_check.instantiation_of works after sizeof rewritingAlasdair Armstrong
2018-01-17Use right effect annotations in early return rewritingThomas Bauereiss
2018-01-17Try to remove early returns more aggressivelyThomas Bauereiss
2018-01-16Fix problem with let-bindings in pattern guardsThomas Bauereiss
2018-01-16Output more type annotations in Lem backendThomas Bauereiss
2018-01-15Support non-trivial literal patternsBrian Campbell
2018-01-12Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-11Ocaml semantics can now run aarch64 hello world example using octapodAlasdair 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-19Support user-defined exceptions in Lem shallow embeddingThomas Bauereiss
2017-12-19Add rewriting step for numeral patternsThomas Bauereiss
2017-12-14An experimental version of sail without bitvector start indexes.Alasdair Armstrong
2017-12-14Fix all compiler warning except in lem pretty printer and monomorphisationAlasdair Armstrong
2017-12-13Use big_nums from LemAlasdair Armstrong
2017-12-07More OCaml test casesAlasdair Armstrong
2017-12-07Fix regressions in OCaml outputAlasdair Armstrong
2017-12-07Functions with guards changes in rewritesBrian Campbell
2017-12-06Add top-level pattern match guards internallyBrian Campbell
2017-12-06Merge remote branch 'experiments' into experimentsThomas Bauereiss
2017-12-05Better support for exceptions in sail for ASL specs that need them.Alasdair Armstrong
2017-12-05Update license headers for Sail sourceAlasdair Armstrong
2017-11-30Improvements to enable parsing and checking intermediate rewritingAlasdair Armstrong
2017-11-28Small update to trivial sizeof rewrites so we can handle all cases inAlasdair Armstrong
2017-11-28Fix issue where statements in blocks had incorrect environmentsAlasdair Armstrong
2017-11-27Split rewriter into separate rewriting library and rewrite passesAlasdair Armstrong