summaryrefslogtreecommitdiff
path: root/riscv/prelude.sail
AgeCommit message (Expand)Author
2018-12-20RISVC model is now at https://github.com/rems-project/sail-riscv . Remove it ...Robert Norton
2018-12-11Fix all tests with type checking changesAlasdair Armstrong
2018-11-29RISC-V: factor the execution trace.Prashanth Mundkur
2018-10-16Re-implement space-related mapping functions in Sail rather than backendsJon French
2018-09-19separate decimal_string_of_bits from string_of_bitsJon French
2018-09-14More monomorphisations for hex_bits_N...Jon French
2018-09-14RISCV prelude: fix typo in ocaml extern for negate_*Jon French
2018-09-14Sail_lib and RISCV prelude: functions for bitwise operations on intsJon French
2018-09-06Coq: fill in a few more RISC-V axiomsBrian Campbell
2018-09-04C: Tweaks to RISC-V to get compiling to CAlasdair Armstrong
2018-08-31Some C stubs for platform bits for RISC-V.Prashanth Mundkur
2018-08-31riscv prelude: yet more manual monomorphisations for hex_bitsJon French
2018-08-30Annotate the RISC-V prelude for C builtins.Prashanth Mundkur
2018-08-15Temporary fix for RISC-V Lem generationBrian Campbell
2018-08-15Get RISC-V on Coq into reasonable state to showBrian Campbell
2018-08-13More RISC-V built-in type constraintsBrian Campbell
2018-08-13RISC-V: mult_range is ill-typed, use mult_atom insteadBrian Campbell
2018-08-13Basic Coq support for RISC-VBrian Campbell
2018-07-11RISC-V model fixes for RMEMJon French
2018-07-10RISCV load-acquire in Lem (-> rmem)Jon French
2018-07-05print to stdout not stderr to stop upsetting rmem regression testsJon French
2018-06-25Support bitlist representation in Sail2_stringThomas Bauereiss
2018-06-11Merge branch 'sail2' into mappingsJon French
2018-05-31Fixes to get ARM u-boot working in Sail.Alasdair Armstrong
2018-05-23riscv decode now uses mapping-decode and passes testsJon French
2018-05-21Add in the platform files and update the ocaml build. Disable the isabelle b...Prashanth Mundkur
2018-05-21further RISCV mapping: all extant non-compressed instructions doneJon French
2018-05-18more riscv mappings; riscv now builds successfully to lem which builds to isa...Jon French
2018-05-15Merge branch 'sail2' into mappingsJon French
2018-05-11further riscv mappingJon French
2018-05-11Remove buggy bit list comparison functions from Lem libraryThomas Bauereiss
2018-05-10more mappingJon French
2018-05-10load-type riscv assemblyJon French
2018-05-10hacky monomorphic bits-string-parser for nowJon French
2018-05-10add space handling mappings to riscv prelude and sail_lib.mlJon French
2018-05-09start of riscv assembly mappingsJon French
2018-04-26Initial support for faults of writes to physical addresses.Prashanth Mundkur
2018-04-26Initial support for faults of reads to physical addresses.Prashanth Mundkur
2018-04-20Add a riscv instruction printer for the execution log.Prashanth Mundkur
2018-04-13Add <=_u to riscv prelude.Prashanth Mundkur
2018-04-09Better separate riscv-independent and riscv-specific parts between prelude an...Prashanth Mundkur
2018-03-19Fixes to C backend for RISCV-compilationAlasdair Armstrong
2018-03-14Make partiality more explicit in library functions of Lem shallow embeddingThomas Bauereiss
2018-03-09Specialise constructors for polymorphic unionsAlasdair Armstrong
2018-03-07Make union types consistent in the ASTAlasdair Armstrong
2018-02-07Add some printing functions to Lem shallow embeddingThomas Bauereiss
2018-02-05riscv: slightly prettier register trace outputRobert Norton
2018-02-02Add M extension to RISCV. Slightly inelegant implementation for now but passi...Robert Norton
2018-01-31Add wrappers around Lem operators using bitvector type classThomas Bauereiss
2018-01-30Fix failing Lem testsAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 20:20:28 +0000