| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2018-07-09 | Patch some potential uses of uninitialised variables in AArch64 | Thomas Bauereiss | |
| 2018-07-09 | Simplify treating of undefined_bool in Lem library | Thomas Bauereiss | |
| Use nondeterministic choice by default instead of a deterministic bitstream generator in the state, which is slightly awkward to reason about, because every use of undefined_boolS changes the state. The previous behaviour can be implemented as Sail code, if desired. Also add a default implementation of internal_pick that nondeterministically chooses an element from a list. | |||
| 2018-07-09 | add riscv_analysis.sail to SAIL_SRCS | Jon French | |
| 2018-07-09 | add LOADRES, STORECON, AMO to analysis | Jon French | |
| 2018-07-09 | Bits for bits of aarch64 in coq | Brian Campbell | |
| 2018-07-09 | Support writes to misa.C in riscv. | Prashanth Mundkur | |
| 2018-07-08 | Make the riscv fetch-execute loop return instead of exiting when done. | Prashanth Mundkur | |
| 2018-07-08 | Move the riscv analysis function into its own file for coverage purposes. | Prashanth Mundkur | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |