summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2019-10-16Now builds arm address translation with clang -target aarch64-none-eabiAlasdair 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-19Change Coq Hoare logic rules to produce nicer preconditionsBrian Campbell
2019-09-19Expand Coq Hoare logic and congruence rules to more operatorsBrian Campbell
2019-09-12Remove unnecessary copies of non-existant files in ocaml backend.Robert Norton
2019-09-02Enable part of a test that's been fixed recently.Brian Campbell
2019-09-02Coq: add properly checked subrange update, reduce importsBrian Campbell
2019-08-30Add a couple of overlooked testsBrian Campbell
2019-08-29Clean up some mono testsBrian Campbell
2019-08-29Turn the two abs_int declarations into overloadsBrian Campbell
2019-08-22Coq: tactics to do rewrites under state monad, simple wp computationBrian Campbell
2019-08-22additional option to tweak Coq output to support user-defined monad:pes20
2019-08-20Merge branch 'sail2' of github.com:rems-project/sail into sail2pes20
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-19Coq: add bools_of_bits_nondet and friends to libraryBrian Campbell
2019-08-14Update testsThomas Bauereiss
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-14Fix bug in mono rewritesThomas Bauereiss
2019-08-14Coq library work for proofs:Brian Campbell
2019-08-13Coq: definitions for cheri128 modelBrian Campbell
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 17:14:33 +0000