| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-01 | utils mapping over mpats/mpexps | Jon French | |
| 2018-05-01 | conversion from parse_ast to ast | Jon French | |
| 2018-05-01 | add to parser | Jon French | |
| 2018-05-01 | add mpats to asts | Jon French | |
| 2018-05-01 | re-indent Initial_check.to_ast_typ | Jon French | |
| 2018-05-01 | starting to also do integer support | Jon French | |
| 2018-05-01 | starting to also do integer support | Jon French | |
| 2018-05-01 | start of string pattern matching: currently only literals | Jon French | |
| 2018-05-01 | fix refactored rewrite_pexp_with_guards (where type information is and is ↵ | Jon French | |
| not...) | |||
| 2018-05-01 | add { ~~fieldname } sugar to record patterns, expanding to { fieldname = ↵ | Jon French | |
| fieldname }\n\nCan't use ~ for this to be exactly like OCaml, as is used for 'not' and explicitly allowed as an identifier | |||
| 2018-05-01 | more refactoring of pexp rewriters | Jon French | |
| 2018-05-01 | Type_check: factor rewrite_pexps_with_guards out of rewrite_defs_pat_lits | Jon French | |
| 2018-05-01 | tidy | Jon French | |
| 2018-05-01 | Use a naming scheme rather than random fresh ids for union anonymous records | Jon French | |
| 2018-05-01 | fix warnings | Jon French | |
| 2018-05-01 | Add anonymous record arms to unions | Jon French | |
| (Preprocessed into a real record type with a fresh id and a reference to that generated record type.) | |||
| 2018-05-01 | cheri256: switch to using absolute address (cursor) instead of offset ↵ | Robert Norton | |
| (relative) representation in capability registers, making register and memory format the same and slightly simplifying code. Next step: use struct representation in registers eliminating many conversions between struct and bits? | |||
| 2018-05-01 | remove unneeded commented out code. | Robert Norton | |
| 2018-05-01 | Implement new CGetAddr instruction. Note that we should possibly rename ↵ | Robert Norton | |
| function getCapCursor to getCapAddr. | |||
| 2018-04-30 | Make make uninstall a bit safer... | Robert Norton | |
| 2018-04-27 | Cheri ISA change in CTestSubset -- ignore sealed bits when testing for ↵ | Robert Norton | |
| subset (aids garbage collection). | |||
| 2018-04-26 | Add riscv SV39 page-table walk. | Prashanth Mundkur | |
| 2018-04-26 | Ensure riscv interrupt delegation does not reduce current privilege. | Prashanth Mundkur | |
| 2018-04-26 | Fix bug introduced in alignment check. | Prashanth Mundkur | |
| 2018-04-26 | Lem: Add Size class annotations for nested bitvector types | Thomas Bauereiss | |
| 2018-04-26 | Initial support for faults of writes to physical addresses. | Prashanth Mundkur | |
| 2018-04-26 | Initial support for faults of reads to physical addresses. | Prashanth Mundkur | |
| 2018-04-26 | Fix bug in rewriting of loops | Thomas Bauereiss | |
| Take into account existential types when determining bounds for the loop variable | |||
| 2018-04-26 | Avoid adding explicit type annotations with generated type variables | Thomas Bauereiss | |
| 2018-04-26 | Make effect propagation in rewriter more efficient | Thomas Bauereiss | |
| Use non-recursive fix_eff_exp instead of recursive propagate_exp_effect, assuming that the effects of subexpressions have already been fixed by the recursive calls of the rewriter. | |||
| 2018-04-26 | Lazily evaluate debugging messages | Thomas Bauereiss | |
| This is meant to increase performance; for example, generating debug messages that include pretty-printed expressions can be very costly, if those expressions are complex (e.g. deeply nested E_internal_plet nodes representing a long sequence of monadic binds). | |||
| 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 | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |