| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2018-06-08 | Coq: some handling of existential types as function return types | Brian Campbell | |
| 2018-06-08 | Coq: add destructuring of atom existentials in patterns | Brian Campbell | |
| Plus test case, broken builtin name | |||
| 2018-06-08 | Coq: track add_typquant change | Brian Campbell | |
| 2018-06-08 | Correct dependencies of bytecode sail | Brian Campbell | |
| 2018-06-08 | Coq: existential and constraint solving work | Brian Campbell | |
| - add existential unpacking for function arguments - add mechanism for using properties for existentially typed top-level values (useful for the typechecking tests) - support for length_list and In in Coq constraint solving | |||
| 2018-06-08 | Coq: some very basic existential support | Brian Campbell | |
| Only single variable in places, only packed at literals and variables, no unpacking | |||
| 2018-06-08 | Coq: fix axiom generation | Brian Campbell | |
| 2018-06-08 | Coq: ignore some currently unsupported tests | Brian Campbell | |
| 2018-06-08 | Coq: update foreach handling, correct field accesses | Brian Campbell | |
| 2018-06-08 | Fill in most Coq built-ins | Brian Campbell | |
| 2018-06-08 | Coq: skip two tests with redundant pattern matches | Brian Campbell | |
| 2018-06-08 | Coq: correct failure on unsupported undefined values | Brian Campbell | |
| 2018-06-08 | Coq: use record update syntax (only single fields work for now) | Brian Campbell | |
| 2018-06-08 | Coq: correct implicitness of type arguments in unions | Brian Campbell | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |