summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-04-06Update sail.tex for wip latex outputAlasdair Armstrong
2018-04-05Fix precedence printing and update aarch64 specAlasdair Armstrong
2018-04-05More work on latex outputAlasdair Armstrong
2018-04-05Cleanup repository by removing old and generated filesAlasdair Armstrong
2018-04-05Add generic prelude library that pulls in various basic sailAlasdair Armstrong
2018-04-04Fix another infinite loop in cast bit_to_bool. Following introduction of eq_b...Robert Norton
2018-04-04Make Type_check.solve do obvious cases immediatelyBrian Campbell
2018-04-04Use solver properly to simplify nexps in mono analysis, Lem printingBrian Campbell
2018-04-04Instantiate type properly when introducing mono castsBrian Campbell
2018-04-04Use valspec equations in monomorphisation analysisBrian Campbell
2018-04-04Tweak Type_check.solve for this branchBrian Campbell
2018-04-04Add a function to find unique solution for constraintsAlasdair Armstrong
2018-04-04Add bitvector casts to funcl bodies when necessaryBrian Campbell
2018-04-04Initial rewrite to move complex nexps in fn sigs into constraintsBrian Campbell
2018-04-04Improve location information in mono dependency errorsBrian Campbell
2018-04-04Use simple equations in function specifications to instantiate tyvarsBrian Campbell
2018-04-03Fix failing ARM testAlasdair Armstrong
2018-04-03Added test cases for builtinsAlasdair Armstrong
2018-03-27Fix infinite loop in cheri/mips cast_unit_vec caused by lack of eq_bit in = o...Robert Norton
2018-03-27print IPS after running cheri model.Robert Norton
2018-03-27remove some unneeded else clauses.Robert Norton
2018-03-23Fix indentation of loops in generated IsabelleThomas Bauereiss
2018-03-23Fix build issueAlasdair Armstrong
2018-03-22Fix cheri MakefileAlasdair Armstrong
2018-03-22Fix C compilation for CHERI and MIPSAlasdair Armstrong
2018-03-22Try removing superfluous returns more aggressively for LemThomas Bauereiss
2018-03-22Tune Lem pretty-printingThomas Bauereiss
2018-03-21Patch AST datatypes in generated Isabelle theoriesThomas Bauereiss
2018-03-21Fix Lem generation for MIPSThomas Bauereiss
2018-03-19Fixes to C backend for RISCV-compilationAlasdair Armstrong
2018-03-15Sail now exits with code 1 when OCaml fails to compile generated codeAlasdair Armstrong
2018-03-15add test that cheri specs build (ocaml).Robert Norton
2018-03-15Some CHERI compilation fixesThomas Bauereiss
2018-03-14WIP Latex formattingAlasdair Armstrong
2018-03-14Add and use execute_branch and execute_branch_pcc functions to align code wit...Robert Norton
2018-03-14rename EXTS and EXTZ to sign_extend and zero_extend because it is more obvios...Robert Norton
2018-03-14Fix toplevel pattern compilationAlasdair Armstrong
2018-03-14Update mono testsBrian Campbell
2018-03-14Machine words extract/update operations arguments are the other way aroundBrian Campbell
2018-03-14Remove unnecessary size_itself_int uses in guards (for Lem)Brian Campbell
2018-03-14Fix compilation for OCaml 4.02Thomas Bauereiss
2018-03-14Fix Lem generation for CHERI-MIPS and Aarch64Thomas Bauereiss
2018-03-14Make partiality more explicit in library functions of Lem shallow embeddingThomas Bauereiss
2018-03-14Add rewriting step for moving execute clauses into auxiliary functionsThomas Bauereiss
2018-03-14Disallow impure global let bindingsThomas Bauereiss
2018-03-14Add address to Write_tag outcomeThomas Bauereiss
2018-03-14Use sets instead of lists for Lem nondeterminism monadThomas Bauereiss
2018-03-14fix riscv build: missing eq_bit implementation.Robert Norton
2018-03-14riscv: disable failing lrsc test for now to make sail2 green.Robert Norton
2018-03-14minor cleanup of load -- we no longer need to separate out by access size bec...Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-14 00:11:50 +0000