summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-21cheri: fix a bug in cfromptr: should give null result when value of rt is ↵Robert Norton
zero not only when rt is the zero register (zr).
2018-05-21Ignore src/share_directory.mlRamana Kumar
src/Makefile suggests this is a generated file
2018-05-18Make named theorem collections of state monad more fine-grainedThomas Bauereiss
2018-05-18Add lemmas about monadic Boolean connectivesThomas Bauereiss
2018-05-18Clean up aarch64_extras.lemThomas Bauereiss
2018-05-18Fix bug in rewriting variable updatesThomas Bauereiss
2018-05-18mips: add support for CP0 Config0.K0 field because a test has appeared for ↵Robert Norton
it. This concerns cache behaviour of kernel segment k0 but since we dont have a cache we just store the value. It could be relevant to RMEM if we ever want to support kernel mode there.
2018-05-18cheri: add support for clc with big immediate (clcbi). This is quite easily ↵Robert Norton
done by making it decode to same CLC ast node and extending length of immediate field to 16 bits. cscbi is not supported as the feeling is that it will not be needed.
2018-05-18use correct inequality for strings.Robert Norton
2018-05-18Add sail_valuesAuxiliary rw theorems to computeLibRamana Kumar
2018-05-18Improve sail-heap dependencies in the HolmakefileRamana Kumar
2018-05-18Update HOL4 snapshotRamana Kumar
2018-05-18Avoid split_on_char function that was introduced in OCaml 4.04. Use Util ↵Robert Norton
version instead and make sure to install util and copy it to ocaml build directory.
2018-05-17build fixes: add back tag effect skips required for mips. Move UART check in ↵Robert Norton
to correct place in main.sail. Remove add_atom and sub_atom from prelude as we get them from arith.sail.
2018-05-17changes to for testing FreeBSD boot on MIPS: allowing loading raw file in ↵Robert Norton
ocaml main so that we can have simboot + kernel. Support UART output only.
2018-05-17Merge branch 'cheri-mono' into sail2Brian Campbell
2018-05-17Clean out old sequential filesBrian Campbell
2018-05-17Fix Isabelle->OCaml wrapperThomas Bauereiss
2018-05-17Refactor main.sailThomas Bauereiss
2018-05-17Remove sequential code againBrian Campbell
2018-05-17Clean up CHERI HOL generation a little tooBrian Campbell
2018-05-17Clean up MIPS for HOL4 a littleBrian Campbell
Move mono_rewrites into lib
2018-05-17Tidy up HOL4 riscv a littleBrian Campbell
2018-05-17Use an intermediate base_monad type alias in Lem,Brian Campbell
resolving the difference in type parameters between the prompt and state monads, and allowing a single output file to be used with either. Normally, the type alias is to the prompt monad, but for HOL4 we use the state monad.
2018-05-16Some minor edits and typo-fixes to the manual, and update the files in the ↵Prashanth Mundkur
riscv model.
2018-05-16Add handwritten script to HolmakefileBrian Campbell
2018-05-16More targeted gitignore for HOL4Brian Campbell
(will do individual models later)
2018-05-16Termination proofs and lemmata for sail_values holRamana Kumar
2018-05-16Ignore .hollogsRamana Kumar
2018-05-16Declare hol automatic termination in sail_valuesRamana Kumar
2018-05-16Add global gitignore entries for HOL4Brian Campbell
2018-05-15Really don't remove those filesBrian Campbell
2018-05-15Fix the ebreak instruction to trap, and remove the now obsolete internal ↵Prashanth Mundkur
exception. This should fix the sbreak test.
2018-05-15Make all of Sail HOL libraries, not just the base heapBrian Campbell
2018-05-14import new build of riscv tests including some new ones that are expected to ↵Robert Norton
pass.
2018-05-14Ignore built files in HOL4 snapshotBrian Campbell
2018-05-14Add missing HOL4 files (and disable overzealous cleaning)Brian Campbell
2018-05-12Add ROOT filesThomas Bauereiss
2018-05-12Add link to README.mdThomas Bauereiss
2018-05-12Update RISC-V snapshotThomas Bauereiss
2018-05-12Fix bug in handling of registers with option typeThomas Bauereiss
Also add test cases and Isabelle lemmas
2018-05-12add -APeter Sewell
2018-05-11Add links in Isabelle snapshot READMEThomas Bauereiss
2018-05-11Add Isabelle snapshot of AArch64 with Brian's monomorphisationThomas Bauereiss
2018-05-11Fix last few links in README.mdAlasdair Armstrong
2018-05-11Fix some links and be more clear about licensingAlasdair Armstrong
2018-05-11Try to fix relative links in README.mdAlasdair Armstrong
2018-05-11Add updated README fileAlasdair Armstrong
2018-05-11Add snapshot of HOL4 output for CHERI and RISC-VBrian Campbell
2018-05-11Add missing document list example to repositoryAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 17:24:26 +0000