summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2020-01-17Merge branch 'coq-bool-props' into sail2Brian Campbell
2020-01-17Keep track of source locations for all IR branchesAlasdair
2020-01-16Allow effects on mappingsAlasdair Armstrong
2020-01-16Cleanup type-checking rule for LEXP_fieldAlasdair Armstrong
2020-01-16Keep track of (non-bit) vectors known to be fixed size in JibAlasdair Armstrong
2020-01-14Basic support to track uncaught exceptions in Sail->CAlasdair
2020-01-10Don't do any C specific name mangling for the cons operator in jib_compileAlasdair Armstrong
2020-01-04Coq: change record field update notation to avoid duplicating termsBrian Campbell
2020-01-03Add Sail pretty-printing of bitfieldsThomas Bauereiss
2019-12-18Make sure we generate literals of precisely the right length for symbolic exe...Alasdair Armstrong
2019-12-13move ott pp to different Makefile rulePeter Sewell
2019-12-13experiment in ott-generated ppPeter Sewell
2019-12-12Fix a little bit of inconsistency in the command line argumentsAlasdair Armstrong
2019-12-10Introduce new bitfield syntax for ASL translationAlasdair Armstrong
2019-12-06Don't introduce uneccesary control flow when compilingAlasdair Armstrong
2019-12-03Prover backends: Expand Int type synonyms in type definitionsThomas Bauereiss
2019-12-01Coq: remove last use and definition of doc_nc_propBrian Campbell
2019-11-29Merge branch 'word-numerals' into sail2Thomas Bauereiss
2019-11-29Tweak generated register_value typeThomas Bauereiss
2019-11-29Coq: switch to boolean predicates for Sail-type propertiesBrian Campbell
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 16:51:58 +0000