| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-04-26 | Add a new SHARE_DIR argument to use when doing opam build. For non-opam ↵ | Robert Norton | |
| builds this defaults to git root. | |||
| 2018-04-26 | Make ocamlbuild assume lem is in path instead of relative to current directory. | Robert Norton | |
| 2018-04-26 | Fix apply_header target with location of LICENSE file. | Robert Norton | |
| 2018-04-26 | Opam packaging: add install and uninstall targets and code to find various ↵ | Robert Norton | |
| files in installed location. | |||
| 2018-04-26 | Remove obsolete mips/cheri rules from sail makefile. These are now built in ↵ | Robert Norton | |
| their respective subdirectories. | |||
| 2018-04-25 | Simplify subtyping check | Alasdair Armstrong | |
| This should make subtyping work better for tuples containing constrained types. Removes the intermediate type-normal-form representation from the subtyping check, and replaces it with Env.canonicalize from the canonical branch. | |||
| 2018-04-25 | Start working on documentation | Alasdair Armstrong | |
| 2018-04-24 | Add some explanations to free monad documentation | Thomas Bauereiss | |
| 2018-04-23 | Make riscv build depend on Makefile updates. | Prashanth Mundkur | |
| 2018-04-23 | Add riscv PTE definitions and access control checks. | Prashanth Mundkur | |
| 2018-04-23 | Merge branch 'rmn30_latex' into sail2 | Robert Norton | |
| 2018-04-23 | Add a cheri128_trace target. | Robert Norton | |
| 2018-04-23 | Fix a discrepancy with spec. about which register number is reported for ↵ | Robert Norton | |
| permissions failure in CBuildCap. | |||
| 2018-04-23 | Fix a problem with 128-bit setCapBounds function revealed by CBuildCap test ↵ | Robert Norton | |
| -- an assertion failure that new bounds are exact. The address of the new cap should have address=base (i.e. offset=0) but this was not being set. This was not previously visible because all other uses of setCapBounds already have address=newBase when calling. | |||
| 2018-04-20 | Fix a typo. | Prashanth Mundkur | |
| 2018-04-20 | Add a riscv instruction printer for the execution log. | Prashanth Mundkur | |
| 2018-04-20 | Some cleanup and comments. | Prashanth Mundkur | |
| 2018-04-20 | Make building of Isabelle heap image optional | Thomas Bauereiss | |
| 2018-04-20 | Allow instantiation of type or order type variables without kind declaration | Brian Campbell | |
| 2018-04-20 | Have sign_extend in common Sail Lem library, use it and zero_extend in | Brian Campbell | |
| mono rewrites | |||
| 2018-04-20 | Fix combined sign-extend-slice operation | Brian Campbell | |
| 2018-04-19 | Fix minor typo. | Prashanth Mundkur | |
| 2018-04-19 | Gloss over UInt/unsigned name difference in monomorphisation | Brian Campbell | |
| 2018-04-19 | Fix bug with function being applied to tuples | Alasdair Armstrong | |
| For some reason there was a desugaring rule that mapped f((x, y)) to f(x, y) in initial_check.ml, this prevented functions and constructors from being applied to tuples. | |||
| 2018-04-19 | more nuanced discussion of generating HOL4 and Coq | Peter Sewell | |
| 2018-04-18 | Remove obsolete comment. | Prashanth Mundkur | |
| 2018-04-18 | Add interrupt prioritization and delegation. | Prashanth Mundkur | |
| 2018-04-18 | Fix mideleg semantics after spec clarification from Andrew Waterman. | Prashanth Mundkur | |
| 2018-04-18 | Use the generated num_of_E function for enum E instead of defining one by hand. | Prashanth Mundkur | |
| 2018-04-18 | Add generated PDF of documentation draft --- comments welcome | Thomas Bauereiss | |
| Placed in lib/isabelle/manual/document.pdf Also fixed a few typos. | |||
| 2018-04-18 | Update mono test script | Brian Campbell | |
| 2018-04-18 | Add first draft of Isabelle library documentation | Thomas Bauereiss | |
| 2018-04-18 | Add a simple Hoare logic for sequential reasoning to the library | Thomas Bauereiss | |
| 2018-04-18 | Fix bug in pretty-printing loops to Lem | Thomas Bauereiss | |
| 2018-04-18 | Add some lemmas about bitvectors | Thomas Bauereiss | |
| Also clean up some library functions a bit, and add some missing failure handling variants of division operations on bitvectors. | |||
| 2018-04-18 | Move a few printing functions to sail_values.lem | Thomas Bauereiss | |
| They are used in various specs and test cases. | |||
| 2018-04-18 | Fix another reference to BK_nat | Alastair Reid | |
| 2018-04-18 | Add a test case for using enum to number function as a cast | Alasdair Armstrong | |
| 2018-04-18 | Fix build on linux | Alasdair Armstrong | |
| Turns out that BSD sed is not a subset of GNU sed, GNU sed doesn't allow a space after the -i option. | |||
| 2018-04-18 | Port to Mac: BSD sed != GNU sed | Alastair Reid | |
| For GNU sed, the extension is optional in sed -i ... But in BSD sed, the extension is mandatory sed -i .bak ... | |||
| 2018-04-18 | Move Lem shl_int, shr_int implementations from aarch64_extras to sail lib | Brian Campbell | |
| (note that they're already declared in lib/arith.sail) | |||
| 2018-04-18 | add some experimental support for latex output in multiple files. | Robert Norton | |
| 2018-04-18 | Rename BK_nat to BK_int to be consistent with source syntax | Alasdair Armstrong | |
| 2018-04-18 | Updates to latex mode for documentation | Alasdair Armstrong | |
| 2018-04-18 | Merge branch 'sail2' of github.com:rems-project/sail into sail2 | Robert Norton | |
| 2018-04-18 | fix bug in permissions test of ctestsubset. | Robert Norton | |
| 2018-04-17 | Implement sret. | Prashanth Mundkur | |
| 2018-04-17 | Hook in the delegated trap handler and remove the old one. | Prashanth Mundkur | |
| 2018-04-17 | Add platform initialization for the new bits of machine state. | Prashanth Mundkur | |
| 2018-04-17 | Separate out the trap handler, and make it use the delegatee privilege. | Prashanth Mundkur | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |