summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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
2019-08-14Use bitvector type in mono rewritesThomas Bauereiss
2019-08-13Coq: fix non-exhaustive pattern match failure in riscv duopodBrian Campbell
2019-08-08Fix machine words againAlasdair Armstrong
2019-08-08Update machine wordsAlasdair Armstrong
2019-08-08Fix bitvectorToFromInterpAlasdair Armstrong
2019-08-08Use bitToFromInterp in bitvectorToFromInterpAlasdair Armstrong
2019-08-08Add same to bitlist representationAlasdair Armstrong
2019-08-08Add bitvectorToFromInterpAlasdair Armstrong
2019-08-05Print effect sets in alphabetical orderAlasdair Armstrong
2019-08-05Remove escape/pure effect restriction for mappingAlasdair Armstrong
2019-08-02Fix all warnings (except for two lem warnings)Alasdair Armstrong
2019-08-02Fix up some edge cases with the bitvector/polyvector splitBrian Campbell
2019-08-01Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-08-01Merge remote-tracking branch 'origin/rv_duopod_fix' into sail2Alasdair Armstrong
2019-07-31Coq: reasoning for until loopsBrian Campbell
2019-07-31Revert "Need to separate out the 0.10 lem library from upcoming 0.11"Alasdair Armstrong
2019-07-31Merge branch 'sail2' into union_barrierAlasdair Armstrong
2019-07-31Updates to function unfolding to support scattered definitionsAlasdair Armstrong
2019-07-29Add type check after descattering to keep type environments up to dateBrian Campbell
2019-07-18Need to separate out the 0.10 lem library from upcoming 0.11Alasdair Armstrong
2019-07-18Add a option to check for a feature symbolAlasdair Armstrong
2019-07-18Add a feature flag for barrier type changeAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:43:00 +0000