summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-08-07Merge branch 'monads' into sail2Brian Campbell
2020-08-07Allow C/IR builds to use mono_rewrites without the rest of monomorphisationBrian Campbell
- also tie following type check to the mono_rewrites flag
2020-08-06Fix for last commitAlasdair
2020-08-06Forbid duplicate top-level letbindingsAlasdair
2020-08-06Fix a small bug with nested structs test in -c2 state apiAlasdair
2020-08-06Merge pull request #81 from julienfreche/get_set_finalAlasdair Armstrong
Generate accessors for scalar types, array of scalars and scalars in struct in the sail state
2020-08-05Generate accessors for scalar types, array of scalars and scalars in struct ↵Julien Freche
in the sail state
2020-08-01update READMEpes20
2020-08-01update READMEpes20
2020-08-01wibpes20
2020-08-01tweak overview picpes20
2020-07-31Update 8.3 readme to point to 8.5 sail-armAlasdair Armstrong
2020-07-31More cleanupAlasdair
2020-07-31Remove old specs that have more up to date versionAlasdair
Move outdated things into old subdirectory
2020-07-15Update duplicate ctor warningAlasdair
2020-07-15Merge pull request #77 from julienfreche/fix_name_instead_of_global_c2Alasdair Armstrong
c2: primop: -O: make sure to pick global or name correctly
2020-07-15Add test files missed from last commitMark Wassell
2020-07-15Prevent creation of variant with existing type id and constructors that ↵Mark Wassell
exist as constructor or function
2020-07-14c2: primop: -O: make sure to pick global or name correctlyJulien Freche
2020-07-02Define extz/s_vec in Sail for non-prover backendsBrian Campbell
2020-06-24Add slice.ml to libsailThomas Bauereiss
2020-06-24Add tagged memory builtins to regfp.sailThomas Bauereiss
Implementations for backends other than Lem not yet implemented/hooked up.
2020-06-23Fix bug with duplicate enum identifiers in patternsAlasdair
2020-06-23Rename coq-sail opam file so that pinning worksBrian Campbell
2020-06-18Report locations for "default order" errorsBrian Campbell
2020-06-17Coq: implement shl_int_1Brian Campbell
2020-06-17Coq: fix rich loop variablesBrian Campbell
Accidentally broken by e1a2b0d2 because the Coq backend looks at the wrong type to decide when a proof is needed.
2020-06-17Make `if cond { ... return() };` assert cond in the type environmentBrian Campbell
Avoids generating an assert expression with an escape effect. Mirrors existing case for `if cond { throw(...); };`. No longer requires `-non_lexical_flow`.
2020-06-17Add test for if-return patternBrian Campbell
(currently supported in nl_flow)
2020-06-16Update INSTALL.mdAlasdair Armstrong
2020-06-14Coq: tidy up scope in libraryBrian Campbell
Helps with Coq 8.11. Also fix BBVDIR default in test script.
2020-06-12Coq: fix matching bug in solverBrian Campbell
2020-06-12Update sailcov readme for option changeAlasdair Armstrong
2020-06-12Merge pull request #70 from rems-project/branch-info-output-fileAlasdair Armstrong
Use output file for generated branch information.
2020-06-12Use output file for generated branch information.Prashanth Mundkur
2020-06-12Remove remove field from opam fileAlasdair
As per https://github.com/ocaml/opam-repository/pull/16573
2020-06-11Coq: specialise the andor solvers to avoid excessive search and solve more goalsBrian Campbell
2020-06-10Prepare Coq library for packagingBrian Campbell
- rename files to get rid of prefix - use -Q to get package name right - add Base.v to make package imports simpler - add opam file for coq package
2020-06-09Add splice.ml to libsailThomas Bauereiss
2020-06-05Generate nice error messages for patterns woth duplicate bindingsAlasdair
2020-06-03Update CHANGELOGAlasdair
2020-06-03Correct compiler version in CI scriptAlasdair
2020-06-03Add a workflow for latest released ocamlAlasdair
2020-06-03Update opam file to opam 2Alasdair
2020-06-03add docker makefile targetjp
2020-06-02Add m4 to 18.04 installAlasdair
It previously installed fine via the build-essential package, so no idea what changed! Plus 20.04 works fine with just build-essential
2020-06-02Add ubuntu 20.04 workflowAlasdair
2020-05-27Try to fix Github CIThomas Bauereiss
Add opam PPA when building on Ubuntu to get opam v2.
2020-05-27Update base64 and yojson dependenciesThomas Bauereiss
2020-05-22Fix atomicity of register field writesAlasdair
Previous merge commit caused some code that was generating register.field = value to instead generate temp = register temp.field = value register = temp This was caused by rewriter changes affecting the ANF form, and the Jib compilation was sensitive to small changes in the ANF form when compiling l-expressions. Rather than applying a band-aid fix in the rewriter this commit re-factors the ANF translation of l-expressions to ensure that the jib compilation is more robust and able to consistently generate the correct l-expressions without introducing additional read-modify-write expressions in the code.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:51:37 +0000