summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
to code gen issue.
2018-07-12make unziping freebsd kernel more robust if run again.Robert Norton
2018-07-12Handle failures during interpreting betterAlasdair Armstrong
Changes to the interpreter to better support constant folding during compilation mean it can now throw exceptions to the caller, allow the caller to handle the error, rather than simply printing an error. This broke the ARM interpreter test because exit() is handled by throwing an Exit exception in the interpreter.
2018-07-12update arm and mips models for new type of write_ram builtin. Also fix c and ↵Robert Norton
interpreter implementations of same.
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
to repeat this if re-generating isabelle before submission.
2018-07-11Add FreeBSD boot to mips test suite.Robert Norton
2018-07-11Fixes to Isabelle snapshotThomas Bauereiss
Remove absolute paths, update Aarch64_extras.thy
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
On second thought, this change should not really make a difference; the CHERI test suite still passes without it. Moreover, using unsigned conversion of the vector argument leads to more convenient lemmas for the provers.
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
Except RISC-V duopod, which doesn't seem to build for me at the moment
2018-07-11Fix off-by-one bugs in monomorphisation rewrites involving bitvector subrangesThomas Bauereiss
CHERI test suite now passes using Isabelle-generated emulator
2018-07-11Fix some signedness bugsThomas Bauereiss
add_vec_int and similar functions in the Lem library used unsigned instead of signed conversion.
2018-07-11Update CHERI code extraction from IsabelleThomas Bauereiss
Also use zero-initialised memory. Apparently some tests access unitialised memory, and the default behaviour of the Lem shallow embedding is to fail in this case.
2018-07-10HOL4 snapshot updateBrian Campbell
2018-07-10Coq MIPS snapshotBrian Campbell
2018-07-10Start adding c-backend bits for riscv.Prashanth Mundkur
2018-07-10Support riscv atomic accesses to mmio regions, used by linux to access ↵Prashanth Mundkur
device registers.
2018-07-10remove sim.dts when anonymising.Robert Norton
2018-07-10Make HOL build properly again for all of the modelsBrian Campbell
2018-07-10RISCV load-acquire in Lem (-> rmem)Jon French
2018-07-10fix constructor typoJon French
2018-07-10Only put static qualifier on valspecs when -static flag is usedAlasdair Armstrong
2018-07-10correct pretty-printing using mappingsJon French
2018-07-10disable printing when compiling to Lem to keep rmem happyJon French
2018-07-10Merge branch 'sail2' of github.com:rems-project/sail into sail2Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 14:54:51 +0000