summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-06-20Coq: port handling of effectful and/or from Lem backendBrian Campbell
2018-06-20Coq: a few more opsBrian Campbell
2018-06-19Minor optimization in ocaml_backend to use ints instead of strings for Big_in...Prashanth Mundkur
2018-06-19Add more detail to riscv execution trace log.Prashanth Mundkur
2018-06-19Coq: use undefined_bitvectorBrian Campbell
2018-06-19Coq: library name update (as we did for Lem)Brian Campbell
2018-06-19Add elf parsing from AlastairAlasdair Armstrong
2018-06-19Improvements to Sail C for booting LinuxAlasdair Armstrong
2018-06-18Mono test script updateBrian Campbell
2018-06-18Add bitvector length constraints to mips inequalitiesBrian Campbell
2018-06-18Coq: better handling of identifiers, esp infix onesBrian Campbell
2018-06-18Separate bitvector access/update from generic vector access in std preludeBrian Campbell
2018-06-18Coq: fix up some comparison operations in preludeBrian Campbell
2018-06-18Coq: update prompt monad wrt LemBrian Campbell
2018-06-15Fix riscv system register initialization.Prashanth Mundkur
2018-06-15Fixes for C RTS for aarch64 no it's split into multiple filesAlasdair Armstrong
2018-06-14rename all lem support files to sail2_foo to avoid conflict with sail1 in rmemJon French
2018-06-14provide impl of int_of_string_opt in Sail_lib to support older Ocaml versionsJon French
2018-06-14Refactor C backend, and split RTS into multiple filesAlasdair
2018-06-13Tracing instrumentation for C backendAlasdair Armstrong
2018-06-13Coq: library updates, informative type errors, fix type aliasesBrian Campbell
2018-06-12Coq: Handle simple top-level type variable definitionsBrian Campbell
2018-06-12Coq: upgrade some errors to report locationsBrian Campbell
2018-06-12Coq: support for range type, along with related existential improvementsBrian Campbell
2018-06-12Coq: add more to libraryBrian Campbell
2018-06-12Prove test_raw_add theorem for init_stateRamana Kumar
2018-06-12Make progress on HOL4 test_raw_addRamana Kumar
2018-06-12Work on HOL symbolic evaluation of installing codeRamana Kumar
2018-06-12Experimentation with PrePost for test_raw_addRamana Kumar
2018-06-12Speculation on executing a CHERI test in HOL4Ramana Kumar
2018-06-11Use riscv platform insns_per_tick to tick the clock.Prashanth Mundkur
2018-06-11Put the riscv model's output on stderr, leaving stdout for the platform termi...Prashanth Mundkur
2018-06-11Update retire semantics for riscv WFI.Prashanth Mundkur
2018-06-11add 'pat as id' mapping-patternsJon French
2018-06-11More efficient bitfield implementationAlasdair Armstrong
2018-06-11Merge branch 'mappings' into sail2Jon French
2018-06-11actually fix exist_pattern testJon French
2018-06-11fix test exist_pattern.sail -- lem needed much more of the stdlib to be importedJon French
2018-06-11Merge branch 'sail2' into mappingsJon French
2018-06-11Add string.sail file to libAlasdair Armstrong
2018-06-11Merge branch 'sail2' into mappingsJon French
2018-06-11change double-caret for string-append-pattern to single caret, since that wou...Jon French
2018-06-11ocaml test prelude: option is now in stdlibJon French
2018-06-11drop now-unnecessary type annotation clutter from riscv decode mappingsJon French
2018-06-11better type inference of union-constructors and mappingsJon French
2018-06-09Increment minstret on instruction retires, and handle the case when the minst...Prashanth Mundkur
2018-06-09Some fixes to counteren handling.Prashanth Mundkur
2018-06-09Fix issue in C_backend, and run C tests with undefined behavior sanitizerAlasdair
2018-06-09Fix issue with catch block return values not being compiled correctlyAlasdair
2018-06-08Fix mmio address matching for clint device.Prashanth Mundkur
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 21:11:20 +0000