| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-23 | Coq: make all pattern matches in the output exhaustive | Brian Campbell | |
| Uses previous stage to deal with (e.g.) guards. New option -dcoq_warn_nonex tells you where all of the extra default cases were added. | |||
| 2018-07-20 | Add assorted comments, consistency fixes and cleanup. | Prashanth Mundkur | |
| 2018-07-18 | Coq: constraint solving improvements | Brian Campbell | |
| Use eauto so that user-added hints are more flexible, example with Replicate in aarch64, dropped zbool to prevent slow proof searches (and preprocessing deals with boolean comparisons now). Report failed constraints after preprocessing; Separate preprocessing tactic out. | |||
| 2018-07-17 | Coq: support effectful function signatures in axiom generation | Brian Campbell | |
| 2018-07-17 | Coq: support returning rich integer types from effectful functions | Brian Campbell | |
| (e.g., coerce_int_nat in aarch64) | |||
| 2018-07-17 | Coq: integer shifts | Brian Campbell | |
| 2018-07-17 | Coq: add printing stubs | Brian Campbell | |
| 2018-07-17 | Coq: handle E_constraint properly | Brian Campbell | |
| Adds missing constraints for aarch64 | |||
| 2018-07-16 | Coq: fix false existential problem | Brian Campbell | |
| 2018-07-16 | Coq: we also unfold length | Brian Campbell | |
| 2018-07-16 | Coq: handle simple type variable matches properly and nat type | Brian Campbell | |
| 2018-07-16 | Coq: add support for more complex atom types | Brian Campbell | |
| As a result, add proof to pow2. | |||
| 2018-07-13 | prepare for new opam release | Robert Norton | |
| 2018-07-13 | Merge branch 'sail2' of github.com:rems-project/sail into sail2 | Brian Campbell | |
| 2018-07-13 | Coq: avoid a couple of common identifiers | Brian Campbell | |
| 2018-07-12 | Add missing builtins needed for cheri128 C. Still doesn't build possibly due ↵ | Robert Norton | |
| to code gen issue. | |||
| 2018-07-12 | make unziping freebsd kernel more robust if run again. | Robert Norton | |
| 2018-07-12 | Handle failures during interpreting better | Alasdair Armstrong | |
| Changes to the interpreter to better support constant folding during compilation mean it can now throw exceptions to the caller, allow the caller to handle the error, rather than simply printing an error. This broke the ARM interpreter test because exit() is handled by throwing an Exit exception in the interpreter. | |||
| 2018-07-12 | update arm and mips models for new type of write_ram builtin. Also fix c and ↵ | Robert Norton | |
| interpreter implementations of same. | |||
| 2018-07-12 | Coq: get rid of syntax error on exception handling | Brian Campbell | |
| 2018-07-12 | Coq: handle all bool conjunctions/disjunctions | Brian Campbell | |
| 2018-07-12 | Coq: more autocast insertion | Brian Campbell | |
| 2018-07-12 | Coq: tuple matching in loops | Brian Campbell | |
| 2018-07-12 | Coq: remove unnecessary constraint on foreach loops | Brian Campbell | |
| 2018-07-12 | Temporarily remove some paragraphs from the manual for anonymisation | Alasdair Armstrong | |
| 2018-07-12 | Coq: more accurate autocast insertion | Brian Campbell | |
| 2018-07-12 | Fix bug for large integers in OCaml compilation | Alasdair Armstrong | |
| 2018-07-12 | Further anonymise manual | Alasdair Armstrong | |
| 2018-07-12 | Minor fix to support OCaml 4.02.3 | Shaked Flur | |
| 2018-07-12 | Fixed a nested comment issue | Shaked Flur | |
| 2018-07-11 | Add fixme note about riscv jalr. | Prashanth Mundkur | |
| 2018-07-11 | Update the exception code for riscv LR after clarification on isa-dev. | Prashanth Mundkur | |
| 2018-07-12 | Fixes for ARM Sail tests, and get_time_ns for interpreter | Alasdair | |
| 2018-07-11 | RISC-V model fixes for RMEM | Jon French | |
| 2018-07-11 | Remove copyright header from generated isabelle for anonymisation. Make sure ↵ | Robert Norton | |
| to repeat this if re-generating isabelle before submission. | |||
| 2018-07-11 | Add FreeBSD boot to mips test suite. | Robert Norton | |
| 2018-07-11 | Fixes to Isabelle snapshot | Thomas Bauereiss | |
| Remove absolute paths, update Aarch64_extras.thy | |||
| 2018-07-11 | Note that a suitable HOL version is required | Brian Campbell | |
| 2018-07-11 | Add ROOTS file to Isabelle snapshot | Thomas Bauereiss | |
| 2018-07-11 | Update Isabelle and HOL snapshots | Thomas Bauereiss | |
| 2018-07-11 | Partially revert change to add_vec_int et al | Thomas Bauereiss | |
| On second thought, this change should not really make a difference; the CHERI test suite still passes without it. Moreover, using unsigned conversion of the vector argument leads to more convenient lemmas for the provers. | |||
| 2018-07-11 | Fix riscv_duopod build. | Robert Norton | |
| 2018-07-11 | Manage expectations about processing time for HOL4 models | Brian Campbell | |
| 2018-07-11 | Update HOL4 snapshot with Thomas' fixes | Brian Campbell | |
| 2018-07-10 | Add an option to specify the dtc to use for the riscv platform. | Prashanth Mundkur | |
| 2018-07-10 | Turn off some riscv debug tracing. | Prashanth Mundkur | |
| 2018-07-11 | Update Isabelle snapshots | Thomas Bauereiss | |
| Except RISC-V duopod, which doesn't seem to build for me at the moment | |||
| 2018-07-11 | Fix off-by-one bugs in monomorphisation rewrites involving bitvector subranges | Thomas Bauereiss | |
| CHERI test suite now passes using Isabelle-generated emulator | |||
| 2018-07-11 | Fix some signedness bugs | Thomas Bauereiss | |
| add_vec_int and similar functions in the Lem library used unsigned instead of signed conversion. | |||
| 2018-07-11 | Update CHERI code extraction from Isabelle | Thomas Bauereiss | |
| Also use zero-initialised memory. Apparently some tests access unitialised memory, and the default behaviour of the Lem shallow embedding is to fail in this case. | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |