summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-31Some tweaks to ocaml compilation and sail_lib for ARM with system registersAlasdair Armstrong
2018-05-31Add auxiliary script to HolmakefileRamana Kumar
2018-05-31Add some HOL4 termination proofs for state.lemRamana Kumar
2018-05-30Fix typo in install instructionsAlasdair Armstrong
2018-05-30Update INSTALL.mdAlasdair Armstrong
Some tweaks to installation instructions for latest OCaml versions (4.05 and 4.06)
2018-05-28Coq: merge some implicit variables from axioms with argumentsBrian Campbell
(Similar to the proper translation for function definitions)
2018-05-28Coq: add back tests with undefined functionsBrian Campbell
2018-05-28Coq: prefer simple binders over patternsBrian Campbell
Otherwise it has occasional problems working out the return type
2018-05-28Coq: add option to produce axioms for unimplemented functionsBrian Campbell
Useful for partial test cases (e.g., some of the typechecking tests) Also a bonus warning for such functions in normal use
2018-05-28Coq: proper printing of nexpsBrian Campbell
2018-05-25Coq: fill in some built-insBrian Campbell
vector_access is a bit hacky at the moment - it expects a constraint to be shown between the index and the list size, but we don't track list sizes in general
2018-05-25Use paged memory storage for ocaml backend memory. This is slightly slower ↵Robert Norton
(<5% on a simple test) but dramatically reduces memory usage compared to having a hash table entry per byte!
2018-05-25allow loading multiple raw files in ocaml main backend to allow kernel and ↵Robert Norton
dtb to be mapped.
2018-05-24Revert "Allow instantiation of type or order type variables without kind ↵Brian Campbell
declaration" This reverts commit 895f868cd537277ba61dfc427fee0e288af7e226. These are actually treated as Ints (although you could pretend they weren't and it mostly worked).
2018-05-24Check kinds of type variables while checking well-formedness of typesBrian Campbell
Stops (e.g.) an Int being used as a Type, including when no kind was declared. The following commit will remove the test for the latter case.
2018-05-24Coq: need None special case here, tooBrian Campbell
2018-05-24Coq: solve more constraintsBrian Campbell
2018-05-24Help launch coqideBrian Campbell
2018-05-24Import (rather hacky) Coq Sail librariesBrian Campbell
2018-05-24Coq: record conditionals in the context for constraint solvingBrian Campbell
2018-05-23Fix incorrect channel in dtc i/o.Prashanth Mundkur
2018-05-23A couple of missing >= 0 constraints on vector handling functionsBrian Campbell
2018-05-23Coq: Implement the most basic merging of type- and term-level parametersBrian Campbell
2018-05-23Fix riscv build for older versions of ocamlbuild (e.g. 4.02.3) by copying ↵Robert Norton
platform ocaml files into _sbuild directory generated by sail and then running ocamlbuild there.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 10:39:33 +0000