summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-07-23AArch64 patches: EL2 secure not implementedAlastair Reid
2018-07-23Coq: faster MIPS extras without confusing messageBrian Campbell
2018-07-23Coq test for a few non-trivial atom typesBrian Campbell
2018-07-23Coq: make all pattern matches in the output exhaustiveBrian Campbell
2018-07-20Add assorted comments, consistency fixes and cleanup.Prashanth Mundkur
2018-07-18Coq: constraint solving improvementsBrian Campbell
2018-07-17Coq: support effectful function signatures in axiom generationBrian Campbell
2018-07-17Coq: support returning rich integer types from effectful functionsBrian Campbell
2018-07-17Coq: integer shiftsBrian Campbell
2018-07-17Coq: add printing stubsBrian Campbell
2018-07-17Coq: handle E_constraint properlyBrian Campbell
2018-07-16Coq: fix false existential problemBrian Campbell
2018-07-16Coq: we also unfold lengthBrian Campbell
2018-07-16Coq: handle simple type variable matches properly and nat typeBrian Campbell
2018-07-16Coq: add support for more complex atom typesBrian Campbell
2018-07-13prepare for new opam releaseRobert Norton
2018-07-13Merge branch 'sail2' of github.com:rems-project/sail into sail2Brian Campbell
2018-07-13Coq: avoid a couple of common identifiersBrian Campbell
2018-07-12Add missing builtins needed for cheri128 C. Still doesn't build possibly due ...Robert Norton
2018-07-12make unziping freebsd kernel more robust if run again.Robert Norton
2018-07-12Handle failures during interpreting betterAlasdair Armstrong
2018-07-12update arm and mips models for new type of write_ram builtin. Also fix c and ...Robert Norton
2018-07-12Coq: get rid of syntax error on exception handlingBrian Campbell
2018-07-12Coq: handle all bool conjunctions/disjunctionsBrian Campbell
2018-07-12Coq: more autocast insertionBrian Campbell
2018-07-12Coq: tuple matching in loopsBrian Campbell
2018-07-12Coq: remove unnecessary constraint on foreach loopsBrian Campbell
2018-07-12Temporarily remove some paragraphs from the manual for anonymisationAlasdair Armstrong
2018-07-12Coq: more accurate autocast insertionBrian Campbell
2018-07-12Fix bug for large integers in OCaml compilationAlasdair Armstrong
2018-07-12Further anonymise manualAlasdair Armstrong
2018-07-12Minor fix to support OCaml 4.02.3Shaked Flur
2018-07-12Fixed a nested comment issueShaked Flur
2018-07-11Add fixme note about riscv jalr.Prashanth Mundkur
2018-07-11Update the exception code for riscv LR after clarification on isa-dev.Prashanth Mundkur
2018-07-12Fixes for ARM Sail tests, and get_time_ns for interpreterAlasdair
2018-07-11RISC-V model fixes for RMEMJon French
2018-07-11Remove copyright header from generated isabelle for anonymisation. Make sure ...Robert Norton
2018-07-11Add FreeBSD boot to mips test suite.Robert Norton
2018-07-11Fixes to Isabelle snapshotThomas Bauereiss
2018-07-11Note that a suitable HOL version is requiredBrian Campbell
2018-07-11Add ROOTS file to Isabelle snapshotThomas Bauereiss
2018-07-11Update Isabelle and HOL snapshotsThomas Bauereiss
2018-07-11Partially revert change to add_vec_int et alThomas Bauereiss
2018-07-11Fix riscv_duopod build.Robert Norton
2018-07-11Manage expectations about processing time for HOL4 modelsBrian Campbell
2018-07-11Update HOL4 snapshot with Thomas' fixesBrian Campbell
2018-07-10Add an option to specify the dtc to use for the riscv platform.Prashanth Mundkur
2018-07-10Turn off some riscv debug tracing.Prashanth Mundkur
2018-07-11Update Isabelle snapshotsThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 23:49:00 +0000