summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-08-24Merge pull request #83 from julienfreche/configure_get_setAlasdair Armstrong
c2: make the global state API configurable for externally defined get/set functions
2020-08-21Add reformat option to SailAlasdair
Reformats input source code using the pretty printer preserving the file structure. Probably not useable as an ocamlformat or rustfmt like tool, but good enough to take generated code without formatting and make it readable.
2020-08-21C generation tweaksAlasdair
2020-08-21c2: make the global state API configurable for externally defined get/set ↵Julien Freche
functions
2020-08-18Move sail_state declaration into it's own fileAlasdair
Useful for RISC-V with it's custom C emulator
2020-08-13Preserve file structure through initial checkAlasdair
Insert $file_start and $file_end pragmas in the AST, as well as $include_start and $include_end pragmas so we can reconstruct the original file structure later if needed, provided nothing like topological sorting has been done. Have the Lexer produce a list of comments whenever it parses a file, which can the be attached to the nearest nodes in the abstract syntax tree.
2020-08-10Fix a C backend bug with letbindings in guards shadowing body definitionsAlasdair
2020-08-07Remove Makefile references to old directoriesBrian Campbell
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 20:58:29 +0000