| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-15 | Merge branch 'sail2' into mappings | Jon French | |
| 2018-05-15 | Really don't remove those files | Brian Campbell | |
| 2018-05-15 | reorder lem rewrite passes and explicitly remove mapping valspecs; string ↵ | Jon French | |
| stuff now compiles to Lem | |||
| 2018-05-15 | rewrite_defs_guarded_pats: guards deserve rewriting too | Jon French | |
| 2018-05-15 | Fix the ebreak instruction to trap, and remove the now obsolete internal ↵ | Prashanth Mundkur | |
| exception. This should fix the sbreak test. | |||
| 2018-05-14 | make debug printing of realised mappings both optional and lazy | Jon French | |
| 2018-05-14 | import new build of riscv tests including some new ones that are expected to ↵ | Robert Norton | |
| pass. | |||
| 2018-05-14 | Ignore built files in HOL4 snapshot | Brian Campbell | |
| 2018-05-14 | Add missing HOL4 files (and disable overzealous cleaning) | Brian Campbell | |
| 2018-05-12 | Add ROOT files | Thomas Bauereiss | |
| 2018-05-12 | Add link to README.md | Thomas Bauereiss | |
| 2018-05-12 | Update RISC-V snapshot | Thomas Bauereiss | |
| 2018-05-12 | Fix bug in handling of registers with option type | Thomas Bauereiss | |
| Also add test cases and Isabelle lemmas | |||
| 2018-05-12 | add -A | Peter Sewell | |
| 2018-05-11 | Add links in Isabelle snapshot README | Thomas Bauereiss | |
| 2018-05-11 | Add Isabelle snapshot of AArch64 with Brian's monomorphisation | Thomas Bauereiss | |
| 2018-05-11 | Fix last few links in README.md | Alasdair Armstrong | |
| 2018-05-11 | Fix some links and be more clear about licensing | Alasdair Armstrong | |
| 2018-05-11 | Try to fix relative links in README.md | Alasdair Armstrong | |
| 2018-05-11 | Add updated README file | Alasdair Armstrong | |
| 2018-05-11 | Add snapshot of HOL4 output for CHERI and RISC-V | Brian Campbell | |
| 2018-05-11 | Add missing document list example to repository | Alasdair Armstrong | |
| 2018-05-11 | Update and alphabetise author list in manual | Alasdair Armstrong | |
| 2018-05-11 | More builtin names in constant propagation | Brian Campbell | |
| 2018-05-11 | Temporary hacks for monomorphisation | Brian Campbell | |
| Mostly introducing type variables for regsize in valspecs | |||
| 2018-05-11 | Make nexp simplification a little smarter | Brian Campbell | |
| (should really make the Lem pretty printer use the solver properly, but this is a useful stopgap) | |||
| 2018-05-11 | Actually use the correct type for singleton rewriting this time | Brian Campbell | |
| 2018-05-11 | Be much more careful to introduce the right bitvector casts to the right sizes | Brian Campbell | |
| 2018-05-11 | Handle automatic existential unpacking in function application in mono analysis | Brian Campbell | |
| 2018-05-11 | Use type from funcl in singleton rewriting | Brian Campbell | |
| The pattern types may be subtypes, using those caused it to try rewriting int parameters and failing | |||
| 2018-05-11 | ...and actually working | Jon French | |
| 2018-05-11 | Add link to Thomas's Sail/Isabelle documentation in manual | Alasdair Armstrong | |
| Replace the old manual with new version in repository root | |||
| 2018-05-11 | further riscv mapping | Jon French | |
| 2018-05-11 | support for mapping-patterns inside (should be) all other pattern types | Jon French | |
| 2018-05-11 | More work on documentation | Alasdair Armstrong | |
| Should have all the main language features covered in at least some detail now. | |||
| 2018-05-11 | Work around Lem generation problem in RISC-V | Thomas Bauereiss | |
| "sum" is an existing constant in Isabelle, and the Lem constant avoiding mechanism does not seem to pick it up when used as the name of a function parameter. | |||
| 2018-05-11 | Add snapshot of generated Isabelle theories | Thomas Bauereiss | |
| Currently contains Lem and Sail libraries, and RISC-V and CHERI-MIPS specs. | |||
| 2018-05-11 | add .git to dev-repo in opam file to satisfy opam-publish. | Robert Norton | |
| 2018-05-11 | prepare sail 0.2 release | Robert Norton | |
| 2018-05-11 | Add uart stub with registers based on ARM uart spec | Alasdair Armstrong | |
| 2018-05-11 | Remove buggy bit list comparison functions from Lem library | Thomas Bauereiss | |
| Found bugs by running CHERI test suite on Isabelle-exported model: signed less-than for bit lists was missing negations for the two's complement, and unsigned less-than compared the reverse lists. Since all other backends implement this in Sail, it seems best to just remove this code. Also add support for infix operators to Lem backend, by z-encoding their identifiers like the other backends do. | |||
| 2018-05-11 | Remove unneeded _sail suffix from latex files. | Robert Norton | |
| 2018-05-11 | Avoid generating latex files that differ only by case because this causes ↵ | Robert Norton | |
| confusion on case insensitive file systems (e.g. mac). | |||
| 2018-05-10 | latex: don't include the prefix in the label. This means we have the option ↵ | Robert Norton | |
| of omitting valspec in documentation if it is deemed too verbose and still have hyperlinks work. The caveat is that it could result in multiply defined labels. | |||
| 2018-05-10 | Document the register_inaccessible function. | Robert Norton | |
| 2018-05-10 | more mapping | Jon French | |
| 2018-05-10 | Type_check: special case appending an empty vector | Jon French | |
| 2018-05-10 | load-type riscv assembly | Jon French | |
| 2018-05-10 | rtype mapping clauses | Jon French | |
| 2018-05-10 | move common mappings to riscv_types.sail | Jon French | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |