| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 2018-07-10 | HOL4 snapshot update | Brian Campbell | |
| 2018-07-10 | Coq MIPS snapshot | Brian Campbell | |
| 2018-07-10 | Start adding c-backend bits for riscv. | Prashanth Mundkur | |
| 2018-07-10 | Support riscv atomic accesses to mmio regions, used by linux to access ↵ | Prashanth Mundkur | |
| device registers. | |||
| 2018-07-10 | remove sim.dts when anonymising. | Robert Norton | |
| 2018-07-10 | Make HOL build properly again for all of the models | Brian Campbell | |
| 2018-07-10 | RISCV load-acquire in Lem (-> rmem) | Jon French | |
| 2018-07-10 | fix constructor typo | Jon French | |
| 2018-07-10 | Only put static qualifier on valspecs when -static flag is used | Alasdair Armstrong | |
| 2018-07-10 | correct pretty-printing using mappings | Jon French | |
| 2018-07-10 | disable printing when compiling to Lem to keep rmem happy | Jon French | |
| 2018-07-10 | Merge branch 'sail2' of github.com:rems-project/sail into sail2 | Robert Norton | |
| 2018-07-10 | remove obsolete files from language directory. | Robert Norton | |
| 2018-07-10 | Update HOL setup | Brian Campbell | |
| 2018-07-10 | Another AArch64 patch | Thomas Bauereiss | |
| Makes CheckAndUpdateDescriptor respect endianness | |||
| 2018-07-10 | Add more Isabelle lemmas to library | Thomas Bauereiss | |
| 2018-07-10 | Tweak to anonymous copyright header. | Robert Norton | |
| 2018-07-10 | further anonymisation work. | Robert Norton | |
| 2018-07-10 | Aarch64 mono script update | Brian Campbell | |
| 2018-07-09 | Initialize fresh memory to 0 in the OCaml backend. | Prashanth Mundkur | |
| This makes it consistent with the C backend, and also makes it easier to compare traces across execution re-runs. | |||
| 2018-07-09 | Log some timing info at the end of riscv execution. | Prashanth Mundkur | |
| 2018-07-09 | Lem: prefer type variables to constants when looking for equivalent nexps | Brian Campbell | |
| If we have an nexp that we can't print, look for an equivalent type variable before looking for a constant - the constant may only be valid locally (e.g., under an if) while the type variable will be valid throughout the function. Fixes a problem with aget_Mem on aarch64. | |||
| 2018-07-09 | Add no_devices.sail to be compatible with latest AArch64 prelude and | Alasdair Armstrong | |
| update aarch64 model | |||
| 2018-07-09 | anonymise another github link. | Robert Norton | |
| 2018-07-09 | anonymise github link in sail manual. | Robert Norton | |
| 2018-07-09 | Remove awkward constraints on GetSlice_int for now | Brian Campbell | |
| 2018-07-09 | Changes for anonymisation. Ensure headers are in correct format. Remove some ↵ | Robert Norton | |
| redundant files. | |||
| 2018-07-09 | Tweak bit casting definitions in MIPS to avoid non-exhaustive patterns | Brian Campbell | |
| Recent change made them proper matches rather than conditionals, and Coq rejects incomplete matches. (Will need a proper solution later...) | |||
| 2018-07-09 | Coq: remove some unnecessary casts | Brian Campbell | |
| 2018-07-09 | Support building an anonymised version of manual. Fix sail example in ↵ | Robert Norton | |
| manual. Remove incomplete types chapter from manual per AA's recommendation. | |||
| 2018-07-09 | Update gitignore | Thomas Bauereiss | |
| 2018-07-09 | Fix bug in rewriting of try-catch-blocks with variable updates | Thomas Bauereiss | |
| 2018-07-09 | Tweak rewriting of literal patterns for Lem | Thomas Bauereiss | |
| 2018-07-09 | Add explanatory comment to guard rewriting | Thomas Bauereiss | |
| 2018-07-09 | Update CHERI code generation from Isabelle | Thomas Bauereiss | |
| 2018-07-09 | Add some syntactic sugar for Isabelle | Thomas Bauereiss | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |