summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-11-30Rename Undefined outcome to ChooseThomas Bauereiss
2018-11-30Improvements for ASL parserAlasdair Armstrong
2018-11-29RISC-V: more tidying up of the Spike interface.Prashanth Mundkur
2018-11-29Add separate outcome/event for tagged memory loadsThomas Bauereiss
2018-11-29RISC-V: implement WFI in the platform model.Prashanth Mundkur
2018-11-29RISC-V: factor the execution trace.Prashanth Mundkur
2018-11-29RISC-V: no ldu for rv64iBrian Campbell
2018-11-29RISC-V: properly set mstatus.FS in absence of floating-point support.Prashanth Mundkur
2018-11-29RISC-V: minor cleanup of the spike interface.Prashanth Mundkur
2018-11-29Update install instructions.Prashanth Mundkur
2018-11-29RISC-V: add some missing constraints on compressed instruction encodingsBrian Campbell
2018-11-29RISC-V: add checks for misaligned targets to jumps and branchesBrian Campbell
2018-11-29Add some helper lemmas to Isabelle libThomas Bauereiss
2018-11-29Merge branch 'rvfi-dii' into sail2Brian Campbell
2018-11-28Allow folding constant expressions into single register readsAlasdair
2018-11-27Fix memory leak in string_of_bitsAlasdair Armstrong
2018-11-27Add an optimisation pass to combine variables if possibleAlasdair Armstrong
2018-11-26Use a temporary definition of List.init until 4.06 is more standard.Prashanth Mundkur
2018-11-26Add random generators for record typesBrian Campbell
2018-11-23Introduce intermediate bitvector representation in CAlasdair Armstrong
2018-11-23C backend improvementsAlasdair Armstrong
2018-11-21RISC-V: allow platform ram size to be configurable.Prashanth Mundkur
2018-11-21Coq: only generate equality functions for records where we need itBrian Campbell
2018-11-21Coq: min_natBrian Campbell
2018-11-21Coq: add equality for records and polymorphic vectorsBrian Campbell
2018-11-21Escape string literals in coq backend. Note that 71020c2f460e6031776df17cf8f2...Robert Norton
2018-11-21Escape strings literals in lem pretty printer.Robert Norton
2018-11-20Use nat instead of (list bitU) for addresses in monad outcomesThomas Bauereiss
2018-11-20Add a test case for a struct with a constrained type variableAlasdair Armstrong
2018-11-20Add messages for assert failures without user defined messagesAlasdair Armstrong
2018-11-20Minor coq updatesBrian Campbell
2018-11-20Add full constraints for vector updatesBrian Campbell
2018-11-19Fix Lem untupling to correctly identify when multiple arguments are usedBrian Campbell
2018-11-19Don't re-check AST repeatedly in exp_lift_assign re-writeAlasdair Armstrong
2018-11-19prep for opam release with new latex.Robert Norton
2018-11-19Commit the Sail file for config register test not the outputAlasdair Armstrong
2018-11-19Ensure sizeof re-writing occurs for configuration registersAlasdair Armstrong
2018-11-19Merge branch 'latex' into sail2Robert Norton
2018-11-19Add missing constraints on bitvector_access, with regression test.Fixes #24.Robert Norton
2018-11-19A few more constraint lemmas for aarch64Brian Campbell
2018-11-16Canonicalise functions types in val specsAlasdair Armstrong
2018-11-16Various bugfixes and a simple profiling feature for rewritesAlasdair Armstrong
2018-11-15document signed and unsignedRobert Norton
2018-11-15When outputing latex do not expand type synonyms in val specs during type check.Robert Norton
2018-11-15Add simple valspec printing in latex that drops effects and other extraneous ...Robert Norton
2018-11-15ast_utils: simplify numeric constraints in inequalities.Robert Norton
2018-11-14Add option to turn off RISC-V compressed instruction supportBrian Campbell
2018-11-14Fix memory map in RVFI-DII modeBrian Campbell
2018-11-14Use code style For [id] refs in doc comments.Robert Norton
2018-11-14latex: use callback macro saildocxxx (one per top-level category) to give use...Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 09:42:57 +0000