summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2017-11-08Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ex...Alasdair Armstrong
2017-11-08Allow for different extern names for different backendsAlasdair Armstrong
2017-11-07Fix typo in constraint rewriterThomas Bauereiss
2017-11-07Add builtin for reversing endiannessThomas Bauereiss
2017-11-07Declare prelude functions as externThomas Bauereiss
2017-11-07Fix vector_subrange typoBrian Campbell
2017-11-03Fix ocaml test suiteAlasdair Armstrong
2017-11-03Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ex...Alasdair Armstrong
2017-11-03Fixed a bug where true and false get mixed up in rewriterAlasdair Armstrong
2017-11-03Fix a bug where sail would throw an exception with empty file listAlasdair Armstrong
2017-11-03Make sure simple parameter sizes appear in Lem mwords outputBrian Campbell
2017-11-03Make nexp_simp a little smarterBrian Campbell
2017-11-02Added monomorphism restriction to undefined values.Alasdair Armstrong
2017-11-02Merge branch 'experiments'Thomas Bauereiss
2017-11-02Fix a few AST and parsing-related bugsThomas Bauereiss
2017-11-02Optionally generate an initial register state for the sequential Lem shallow ...Thomas Bauereiss
2017-11-02Fix translation of repeat-until loops to LemThomas Bauereiss
2017-11-02Handle "undefined" type-level sizes in monomorphisationBrian Campbell
2017-11-01Support bitvector-size-parametric functions in Lem outputBrian Campbell
2017-11-01Fix some missing nexp simplification in Lem outputBrian Campbell
2017-10-31Fixed wrong image for List-remove.svgAlasdair Armstrong
2017-10-31Added trace viewer application for traces produced by sail -ocaml_traceAlasdair Armstrong
2017-10-31Improvements to register read tracing in ocaml backendAlasdair Armstrong
2017-10-31Pretty-print Sail assertions in LemThomas Bauereiss
2017-10-31Fix bug in topological sorting of val-specsThomas Bauereiss
2017-10-31Remove redundant nexp simplification functionThomas Bauereiss
2017-10-27Fixed some ocaml backend related bugsAlasdair Armstrong
2017-10-26Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ex...Alasdair Armstrong
2017-10-26Unfold nexp abbreviations for pretty-printingThomas Bauereiss
2017-10-26Update val specs after rewriting functionsThomas Bauereiss
2017-10-26Experiment with pretty-printing non-atomic nexps in LemThomas Bauereiss
2017-10-26Updated ocaml backend so tracing instrumentation is optional.Alasdair Armstrong
2017-10-25Allow mutually recursive functionsThomas Bauereiss
2017-10-25Point sail/src makefile at ott file in language/Alasdair Armstrong
2017-10-25List.cons is too newBrian Campbell
2017-10-25Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-25Generate ast.ml from ott file and update makefile.Alasdair Armstrong
2017-10-25Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-25Alternative low-memory version of barrier_kindCompareBrian Campbell
2017-10-25Avoid name clash in generated LemBrian Campbell
2017-10-24Make nexp simplifier handle recursion properlyBrian Campbell
2017-10-24More succinct syntax in new parser for externed valspecs which shareAlasdair Armstrong
2017-10-24Print type annotations in Lem with type variablesBrian Campbell
2017-10-24Limit quantifiers printed in Lem to type variables that actuallyBrian Campbell
2017-10-24Handle existential types in Lem backend by stripping them andBrian Campbell
2017-10-24Generate undefined_bitvector function when targeting machine wordsBrian Campbell
2017-10-24Produce debug message when an expression can't be converted to a constraintBrian Campbell
2017-10-24Remove special case for boolean (as opposed to bool)Brian Campbell
2017-10-23Type check external castsBrian Campbell
2017-10-23Added effect set pretty printing for new parserAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 14:28:37 +0000