aboutsummaryrefslogtreecommitdiff
path: root/handwritten_support
AgeCommit message (Expand)AuthorFilesLines
2019-07-18Make sure everything builds correctlyAlasdair Armstrong2-45/+79
2019-07-18Revert "Support DMB/DSB domains"Alasdair Armstrong2-22/+22
2019-07-18Support DMB/DSB domainsShaked Flur2-22/+22
2019-06-24Add PMP checks to physical memory accesses.Prashanth Mundkur2-0/+8
2019-04-25Fix coq build.Prashanth Mundkur1-19/+19
2019-04-25riscv_extras.lem: update read/write_mem calls with (dummy) addrsize argumentJon French1-18/+18
2019-04-10Update Coq memory interfacesBrian Campbell1-20/+27
2019-04-04Add `sys_enable_writable_misa` and `sys_enable_rvc` to Coq extras fileBrian Campbell1-0/+3
2019-04-03Tweak print_* bindings for LemThomas Bauereiss2-0/+6
2019-04-01Add missed lem definitions for sys misa/rvcflags.Prashanth Mundkur2-0/+16
2019-02-26Restore riscv_extras damaged by merge.Prashanth Mundkur1-9/+13
2019-02-13Make repository have shape RMEM expectsAlasdair Armstrong4-3/+140
2019-02-13Switch version of riscv_extras.lem depending on Sail versionAlasdair Armstrong1-0/+137
2019-01-22Add build Makefile targets for prover backendsThomas Bauereiss1-4/+6
2019-01-21Output auxiliary Isabelle theories into generated_definitions/isabelleThomas Bauereiss1-2/+2
2019-01-19Moved gen/ to handwritten_support/hgenShaked Flur19-0/+1367
2019-01-16More reorg.Prashanth Mundkur5-0/+439
generated by cgit v1.1 at 2024-11-06 03:09:18 +0000