summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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-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
2017-10-23Added support for better tracing in ocaml backendAlasdair Armstrong
2017-10-23Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-19Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experimentsThomas Bauereiss
2017-10-19Fix pretty-printing of type abbreviation definitions with argumentsThomas Bauereiss
2017-10-19Mangle names with '#' characters in Lem pretty-printingThomas Bauereiss
2017-10-19Rewrite undefined values, add type annotations to early returnsThomas Bauereiss
2017-10-19Make some potentially non-terminating library functions terminateThomas Bauereiss
2017-10-19Preserve more type environment information during rewritingThomas Bauereiss
2017-10-19Follow AST changes in (Lem) pretty-printersThomas Bauereiss
2017-10-18Fixes and updates to ocaml backend to compile aarch64_no_vectorAlasdair Armstrong
2017-10-18Merge branch 'experiments' of Peter_Sewell/sail into mono-experimentsBrian Campbell
2017-10-13Handle bitvector_access in constant propagationBrian Campbell
2017-10-13Make Sail_values.repeat total, and remove duplicateBrian Campbell
2017-10-13Fix some bugs that surfaced in the ASL exportThomas Bauereiss
2017-10-13Add rewriting step for tuple-vector assignmentsThomas Bauereiss
2017-10-13Add rewriting step for function effect propagationThomas Bauereiss
2017-10-13Name (bit)vector operations more explicitlyThomas Bauereiss
2017-10-13Add support for real numbers to Lem backendThomas Bauereiss
2017-10-13Improve debugging outputThomas Bauereiss
2017-10-13Repeat and while loops in menhir parser and pretty printerAlasdair Armstrong
2017-10-12Fixes pattern matching exact values ([:'n:]) on integer literalsAlasdair Armstrong
2017-10-10More improvements to menhir parserAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:58:56 +0000