summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-09-12Docs: Mention "opam pin" and reword a detailColumbus240
opam pin is useful in the development workflow. About the rewording: The tests of Sail check the behavior of Sail and not whether it is installed correctly, because the instructions above that paragraph don’t install Sail, they just build it. These circumstances weren’t represented appropriately by the text.
2020-09-12Merge some of the gitignore filesColumbus240
Both /.gitignore and /lib/coq/.gitignore ignored some files in /lib/coq. This commit removes /lib/coq/.gitignore and moves all ignore-statements to /.gitignore . This should simplify the maintenance of gitignore files. The situation with /test/mono/.gitignore is analogous.
2020-09-12gitignore test artifacts of c and coq testsColumbus240
The "c" tests produce some *.h files that didn’t get ignored. The "coq" tests also produce some files that weren’t ignored.
2020-09-12Note in docs that some tests require cvc4Columbus240
2020-09-07Fix typo a mono_rewrites definitionBrian Campbell
- add tests for a couple of related rewrites - accept same range of constants for sign extension in the rewrite as for the zero extension version (to make the test simpler)
2020-09-07Correct external declaration in mono_rewritesBrian Campbell
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 23:46:32 +0000