summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2019-12-03Prover backends: Expand Int type synonyms in type definitionsThomas Bauereiss
2019-11-29Merge branch 'word-numerals' into sail2Thomas Bauereiss
2019-11-29Tweak generated register_value typeThomas Bauereiss
2019-11-26Allow overriding of generated mapping functionsThomas Bauereiss
2019-11-25Merge branch 'hol-regstate' into sail2Thomas Bauereiss
2019-11-21Fix bugs in mutrec constant propagationThomas Bauereiss
2019-11-21Mono: Use more environment information when adding bitvector castsThomas Bauereiss
2019-11-21Add option to generate grouped register state recordThomas Bauereiss
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-14Fix typo in constant folding for and_bool/or_boolAlasdair Armstrong
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-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-01More work on GDB interfaceAlasdair 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-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-25Allow interactive commands to be setup outside isail.mlAlasdair Armstrong
2019-10-24Coq: use `abstract` to separate out proofs from definitionsBrian Campbell
2019-10-17Allow generating C that doesn't hard code any librariesAlasdair Armstrong
2019-10-16Make nostd Sail arena allocator thread safe (maybe)Alasdair
2019-10-15More work on bare-metal SailAlasdair Armstrong
2019-10-14Add -Ofixed_int and -Ofixed_bits to assume fixed-precision ints and bitvector...Alasdair Armstrong
2019-10-02Coq: generate decidable equality instances for variant typesBrian Campbell
2019-10-02Coq: limited support for existentially-typed tuplesBrian Campbell
2019-09-12Remove unnecessary copies of non-existant files in ocaml backend.Robert Norton
2019-08-22additional option to tweak Coq output to support user-defined monad:pes20
2019-08-20add -coq_alt_modules option to override the default imported modulespes20
2019-08-20add -coq_alt_modules option to override the default imported modulespes20
2019-08-20add -coq_alt_modules option to override the default imported modulespes20
2019-08-14Add a mono rewrite for (ones(n) @ zeros(m))Thomas Bauereiss
2019-08-14Inline reg_deref in Lem outputThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 01:04:02 +0000