| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-20 | Coq: a few more ops | Brian Campbell | |
| 2018-06-19 | Minor optimization in ocaml_backend to use ints instead of strings for ↵ | Prashanth Mundkur | |
| Big_int literals. Improves tests/riscv duration by around 2% and size of riscv.o by 15%. | |||
| 2018-06-19 | Add more detail to riscv execution trace log. | Prashanth Mundkur | |
| 2018-06-19 | Coq: use undefined_bitvector | Brian Campbell | |
| 2018-06-19 | Coq: library name update (as we did for Lem) | Brian Campbell | |
| 2018-06-18 | Mono test script update | Brian Campbell | |
| (still need to sort out some string stuff, though) | |||
| 2018-06-18 | Add bitvector length constraints to mips inequalities | Brian Campbell | |
| to match new constraints in prelude | |||
| 2018-06-18 | Coq: better handling of identifiers, esp infix ones | Brian Campbell | |
| 2018-06-18 | Separate bitvector access/update from generic vector access in std prelude | Brian Campbell | |
| (necessary for backends where they're different) Coq uint/sint and related fixes | |||
| 2018-06-18 | Coq: fix up some comparison operations in prelude | Brian Campbell | |
| 2018-06-18 | Coq: update prompt monad wrt Lem | Brian Campbell | |
| 2018-06-15 | Fix riscv system register initialization. | Prashanth Mundkur | |
| 2018-06-14 | rename all lem support files to sail2_foo to avoid conflict with sail1 in rmem | Jon French | |
| 2018-06-14 | provide impl of int_of_string_opt in Sail_lib to support older Ocaml versions | Jon French | |
| 2018-06-13 | Coq: library updates, informative type errors, fix type aliases | Brian Campbell | |
| (The last bit is to declare type aliases as Type so that Coq uses the type scope for notation, so * is prod, not multiplication). | |||
| 2018-06-12 | Coq: Handle simple top-level type variable definitions | Brian Campbell | |
| (also another error reporting improvement) | |||
| 2018-06-12 | Coq: upgrade some errors to report locations | Brian Campbell | |
| 2018-06-12 | Coq: support for range type, along with related existential improvements | Brian Campbell | |
| Plus - Complete solver support for inequalities - Reduce exponentials in solver | |||
| 2018-06-12 | Coq: add more to library | Brian Campbell | |
| 2018-06-12 | Prove test_raw_add theorem for init_state | Ramana Kumar | |
| It can be proved almost entirely by symbolic execution (in <15s) _if_ the right definitions are in the compset. It took a lot of interactive stumbling about to discover that LUPDATE was missing from the standard list compset. | |||
| 2018-06-12 | Make progress on HOL4 test_raw_add | Ramana Kumar | |
| The proof now gets through simulation of the first instruction of the test. | |||
| 2018-06-12 | Work on HOL symbolic evaluation of installing code | Ramana Kumar | |
| 2018-06-12 | Experimentation with PrePost for test_raw_add | Ramana Kumar | |
| 2018-06-12 | Speculation on executing a CHERI test in HOL4 | Ramana Kumar | |
| 2018-06-11 | Use riscv platform insns_per_tick to tick the clock. | Prashanth Mundkur | |
| 2018-06-11 | Put the riscv model's output on stderr, leaving stdout for the platform ↵ | Prashanth Mundkur | |
| terminal. | |||
| 2018-06-11 | Update retire semantics for riscv WFI. | Prashanth Mundkur | |
| 2018-06-11 | add 'pat as id' mapping-patterns | Jon French | |
| 2018-06-11 | Merge branch 'mappings' into sail2 | Jon French | |
| 2018-06-11 | actually fix exist_pattern test | Jon French | |
| 2018-06-11 | fix test exist_pattern.sail -- lem needed much more of the stdlib to be imported | Jon French | |
| 2018-06-11 | Merge branch 'sail2' into mappings | Jon French | |
| 2018-06-11 | Add string.sail file to lib | Alasdair Armstrong | |
| 2018-06-11 | Merge branch 'sail2' into mappings | Jon French | |
| (involved some manual tinkering with gitignore, type_check, riscv) | |||
| 2018-06-11 | change double-caret for string-append-pattern to single caret, since that ↵ | Jon French | |
| wouldn't be legal in a pattern anyway | |||
| 2018-06-11 | ocaml test prelude: option is now in stdlib | Jon French | |
| 2018-06-11 | drop now-unnecessary type annotation clutter from riscv decode mappings | Jon French | |
| 2018-06-11 | better type inference of union-constructors and mappings | Jon French | |
| 2018-06-09 | Increment minstret on instruction retires, and handle the case when the ↵ | Prashanth Mundkur | |
| minstret CSR is explicitly written to. | |||
| 2018-06-09 | Some fixes to counteren handling. | Prashanth Mundkur | |
| 2018-06-09 | Fix issue in C_backend, and run C tests with undefined behavior sanitizer | Alasdair | |
| 2018-06-09 | Fix issue with catch block return values not being compiled correctly | Alasdair | |
| This should fix the issue raised in commit 45554f Adds a test loop_exception that tests throwing exceptions in loops, various looping constructs, and returning values from try/catch blocks. Also modified the test-suite to test C compiled output both with and without optimisations | |||
| 2018-06-08 | Fix mmio address matching for clint device. | Prashanth Mundkur | |
| 2018-06-08 | Add counteren registers. | Prashanth Mundkur | |
| 2018-06-08 | Slightly condense execution trace log. | Prashanth Mundkur | |
| 2018-06-08 | Update initialization of misa. | Prashanth Mundkur | |
| 2018-06-08 | Make the simulation loop use the platform interface to detect exits via htif. | Prashanth Mundkur | |
| 2018-06-08 | Add mem and mmio access tracing. | Prashanth Mundkur | |
| 2018-06-08 | Fix use of non-tail-recursive calls in elf_loader. | Prashanth Mundkur | |
| 2018-06-08 | type checking mappings: allow inferring based on the other side's id inferences | Jon French | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |