summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-22Fix one part of cast introduction, leave another for laterBrian Campbell
2018-05-22Re-enable the RISC-V lem build, and switch the test-suite to use the ↵Prashanth Mundkur
platform build.
2018-05-22Fix for E_cons not being compiled correctly into OCamlAlasdair Armstrong
2018-05-22Fix Lem build for RISC-VThomas Bauereiss
2018-05-21Fix a doc typo.Prashanth Mundkur
2018-05-21Add the missed _tags file, and fix a typo.Prashanth Mundkur
2018-05-21Start platform execution at the reset-vector in the rom.Prashanth Mundkur
2018-05-21Add in the platform files and update the ocaml build. Disable the isabelle ↵Prashanth Mundkur
build until we add suitable platform definitions/stubs. The platform bits are not yet hooked into the model, but only into the build, so are untested.
2018-05-21Add an -ocaml-nobuild option to avoid building the generated ocaml by ↵Prashanth Mundkur
default (off by default).
2018-05-21Move the top-level loop from main to riscv_step, but remove elf bits.Prashanth Mundkur
2018-05-21Move mem-op-result to _sys to be usable from _platform.Prashanth Mundkur
2018-05-21Get Aarch64 exported to HOL4Brian Campbell
Worked around problem with the model where it tries to use bound variables in patterns
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 13:27:55 +0000