summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2018-07-10remove obsolete files from language directory.Robert Norton
2018-07-10Update HOL setupBrian Campbell
2018-07-10Another AArch64 patchThomas Bauereiss
Makes CheckAndUpdateDescriptor respect endianness
2018-07-10Add more Isabelle lemmas to libraryThomas Bauereiss
2018-07-10Tweak to anonymous copyright header.Robert Norton
2018-07-10further anonymisation work.Robert Norton
2018-07-10Aarch64 mono script updateBrian Campbell
2018-07-09Initialize fresh memory to 0 in the OCaml backend.Prashanth Mundkur
This makes it consistent with the C backend, and also makes it easier to compare traces across execution re-runs.
2018-07-09Log some timing info at the end of riscv execution.Prashanth Mundkur
2018-07-09Lem: prefer type variables to constants when looking for equivalent nexpsBrian Campbell
If we have an nexp that we can't print, look for an equivalent type variable before looking for a constant - the constant may only be valid locally (e.g., under an if) while the type variable will be valid throughout the function. Fixes a problem with aget_Mem on aarch64.
2018-07-09Add no_devices.sail to be compatible with latest AArch64 prelude andAlasdair Armstrong
update aarch64 model
2018-07-09anonymise another github link.Robert Norton
2018-07-09anonymise github link in sail manual.Robert Norton
2018-07-09Remove awkward constraints on GetSlice_int for nowBrian Campbell
2018-07-09Changes for anonymisation. Ensure headers are in correct format. Remove some ↵Robert Norton
redundant files.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 10:13:24 +0000