summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-09-02Consider case expressions in early return rewriteThomas Bauereiss
2020-08-27Ignore file start/end pragmas in spliceBrian Campbell
2020-08-27Perform truncation of hex literals for C backend (really for isla)Brian Campbell
For example, if a 129-bit capability is given as a 132-bit hex literal and truncated, this produces a 129-bit binary literal. In isla, this will keep all of the computation concrete because 129-bit concrete values are supported.
2020-08-26Coq: replace other uses of omega with liaBrian Campbell
Also remove omega workaround that lia doesn't need.
2020-08-26Coq: replace a lot of omega with liaBrian Campbell
2020-08-26Coq: Use proof mode for a couple of Fixpoints to avoid Coq 8.12 issueBrian Campbell
2020-08-26Coq: make some uses of auto in the library more robustBrian Campbell
2020-08-25Add function sail_set_coverage_file to sail_coverage headerAlasdair
Can be set by C emulator to control where coverage information is written
2020-08-24Reformat tweaksAlasdair
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 08:59:58 +0000