summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-01-07Coq: accelerate wp steps by improving application of existing specsBrian Campbell
2020-01-04Coq: change record field update notation to avoid duplicating termsBrian Campbell
2019-12-19Coq library improvementsBrian Campbell
2019-12-09Coq: improve solver enough to handle arm specBrian Campbell
2019-12-06Coq: use proof irrelevance for a few propertiesBrian Campbell
2019-12-05Coq: more solving support for boolean predicatesBrian Campbell
2019-12-01Coq: remove last use and definition of doc_nc_propBrian Campbell
2019-11-29Coq: switch to boolean predicates for Sail-type propertiesBrian Campbell
2019-11-21Bump version for release.Robert Norton
2019-11-21Implement -cycle-limit option for OCaml emulator similar to one for C.Robert Norton
2019-11-20Allow undefined values in IR for SMT generationAlasdair Armstrong
2019-11-20Coq: port a couple of definitions from Isabelle for address translation specBrian Campbell
2019-11-14Update location of sail2_instr_kinds.lemRobert Norton
2019-11-14Perform isabelle check only when heap-img rule is used to avoid calling opam ...Robert Norton
2019-11-14Fix typo in constant folding for and_bool/or_boolAlasdair Armstrong
2019-11-13Coq: more proof supportBrian Campbell
2019-11-11Make sure undefined_gen inserts enough type annotations for union constructorsAlasdair Armstrong
2019-11-11Update libsail slightly with recent changesAlasdair Armstrong
2019-11-11Make sure we include LEXP_cast register refs when slicing the specificationAlasdair Armstrong
2019-11-08Refactor Jib compilationAlasdair Armstrong
2019-11-07Make the world a slightly more sane and consistent placeAlasdair Armstrong
2019-11-07Fix Jenkins buildAlasdair Armstrong
2019-11-07Backport fixes to SMT generation from poly_mapping branchAlasdair Armstrong
2019-11-06Allow specifying specific fields of a register as constant with :fixed_regist...Alasdair Armstrong
2019-11-06Add toplevel commands to fix specific register values and simply spec accordi...Alasdair Armstrong
2019-11-05Forbid types declared after a scattered union being used in clausesAlasdair
2019-11-05Improve type error for recursive types slightlyAlasdair Armstrong
2019-11-05Make sure we correctly forbid recursive datatypes that we don't want to supportAlasdair Armstrong
2019-11-04Allow overriding the interpreter effectsAlasdair Armstrong
2019-11-04Some almost-forgotten mono testsBrian Campbell
2019-11-04Coq: compatiblity with 8.10 as well as 8.9Brian Campbell
2019-11-01More work on GDB interfaceAlasdair Armstrong
2019-11-01Update riscv example in manual to make it currentAlasdair Armstrong
2019-11-01Add a missing well-formedness checkAlasdair
2019-10-31Allow sail to be scripted using sailAlasdair
2019-10-31Allow sail interactive toplevel to connect to a running QEMU instance using G...Alasdair Armstrong
2019-10-29add simple html syntax highlighter based on prism.jsjp
2019-10-28Fix jib.ott and SMT regressionsAlasdair Armstrong
2019-10-28Make sure that interactive.ml doesn't transitively depend on lem definitionsAlasdair Armstrong
2019-10-28Coq: label fixpoint bodies, tweak spacingBrian Campbell
2019-10-28Some C backend refactoringAlasdair
2019-10-25Remove global symbol generatorAlasdair
2019-10-25Refactor Jib IR pretty printerAlasdair Armstrong
2019-10-25Some more interpreter tweaksAlasdair Armstrong
2019-10-25Coq: clean up some formattingBrian Campbell
2019-10-25Coq: make sure solver can't accidentally use recursive definitionsBrian Campbell
2019-10-25Allow interactive commands to be setup outside isail.mlAlasdair Armstrong
2019-10-24Coq: use `abstract` to separate out proofs from definitionsBrian Campbell
2019-10-18Coq: tweak a state monad lifting rule to improve performanceBrian Campbell
2019-10-17Allow generating C that doesn't hard code any librariesAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:52:09 +0000