summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-11-02Added monomorphism restriction to undefined values.Alasdair Armstrong
2017-11-02remove a lot of dead code form run_with_elf_cheri*Robert Norton
2017-11-02Merge branch 'experiments'Thomas Bauereiss
2017-11-02reset inCCallDelay in code that is not dead.Robert Norton
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-01workaound for another odd interpreter error where top level let variable got ...Robert Norton
2017-11-01added RISC-V "fence r,r"Shaked Flur
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-31work around interpreter crash by adding cast. Likely this kind of thing will ...Robert Norton
2017-10-31Pretty-print Sail assertions in LemThomas Bauereiss
2017-10-31cheri: throw an exception if there is an attempt to access C26/IDC in the del...Robert Norton
2017-10-31Fix bug in topological sorting of val-specsThomas Bauereiss
2017-10-31Remove redundant nexp simplification functionThomas Bauereiss
2017-10-31cheri: ccall selector 1 should have a branch delay slot. TODO we need to thro...Robert Norton
2017-10-27Fixed some ocaml backend related bugsAlasdair Armstrong
2017-10-26Fix a bug in Sail OCaml libraryAlasdair 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-26fixed release acquire semantics of AMOsShaked Flur
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-25ast.ml generated from l2.ott compiles with rest of ./srcMark Wassell
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-24fix default cap value on cheri128 following previous changes -- E stored in r...Robert Norton
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-23cheri: Null capability should have maximum length, because in cheri128 we wan...Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 08:47:23 +0000