summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2018-06-08Add counteren registers.Prashanth Mundkur
2018-06-08Slightly condense execution trace log.Prashanth Mundkur
2018-06-08Update initialization of misa.Prashanth Mundkur
2018-06-08Make the simulation loop use the platform interface to detect exits via htif.Prashanth Mundkur
2018-06-08Add mem and mmio access tracing.Prashanth Mundkur
2018-06-08Fix use of non-tail-recursive calls in elf_loader.Prashanth Mundkur
2018-06-08type checking mappings: allow inferring based on the other side's id inferencesJon French
2018-06-08Coq: some handling of existential types as function return typesBrian Campbell
2018-06-08Coq: add destructuring of atom existentials in patternsBrian Campbell
2018-06-08Coq: track add_typquant changeBrian Campbell
2018-06-08Correct dependencies of bytecode sailBrian Campbell
2018-06-08Coq: existential and constraint solving workBrian Campbell
2018-06-08Coq: some very basic existential supportBrian Campbell
2018-06-08Coq: fix axiom generationBrian Campbell
2018-06-08Coq: ignore some currently unsupported testsBrian Campbell
2018-06-08Coq: update foreach handling, correct field accessesBrian Campbell
2018-06-08Fill in most Coq built-insBrian Campbell
2018-06-08Coq: skip two tests with redundant pattern matchesBrian Campbell
2018-06-08Coq: correct failure on unsupported undefined valuesBrian Campbell
2018-06-08Coq: use record update syntax (only single fields work for now)Brian Campbell
2018-06-08Coq: correct implicitness of type arguments in unionsBrian Campbell
2018-06-08Add missing Coq builtin info to vector_incBrian Campbell
2018-06-08add sail as dependency of mips targets.Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 12:50:56 +0000