summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2018-07-07Coq: bbv have reorganised their repositoryBrian Campbell
2018-07-07Coq: precise generic vectorsBrian Campbell
2018-07-07Coq: supply index constraint in for loopsBrian Campbell
2018-07-07Coq: eq_range should take proofsBrian Campbell
2018-07-06Coq: use List.In predicates in constraint solving; make other bits robustBrian Campbell
2018-07-05Fix equality comparisons for variants in CAlasdair
2018-07-05Coq: get index_list rightBrian Campbell
2018-07-05Fix equality comparisons for structsAlasdair
2018-07-05restore missing RISC-V fence types in sail2; ignore io bits in fences more cl...Jon French
2018-07-02Coq: add some string functionsBrian Campbell
2018-07-02Coq: replace simpl in a tactic with a more precise "change"Brian Campbell
2018-06-30RTS: fix replicate_bitsAlastair Reid
2018-06-30RTS: Add length asserts to bits opsAlastair Reid
2018-06-30Fix an issue with vector_update_subrangeAlasdair
2018-06-29RTS: tweak TIMEOUT messageAlastair Reid
2018-06-28RTS: Fix utterly broken command line parsingAlastair Reid
2018-06-28RTS: Add --verbosity flag to C modelAlastair Reid
2018-06-28Add tagged memory to C rts to cheri can be compiled to CAlasdair Armstrong
2018-06-28Fix warning in rts.cRobert Norton
2018-06-28Add option to build ocaml with bisect_ppx coverage support. Add cheri targets...Robert Norton
2018-06-28RTS: Add missing #includeAlastair Reid
2018-06-27RTS/Main: tweaking cycle counter handlingAlastair Reid
2018-06-27Actually fix real literals, and add a test for various propertiesAlasdair Armstrong
2018-06-27Fix reading reals from strings in C libAlasdair Armstrong
2018-06-27libsail: optimise real_powerAlastair Reid
2018-06-27Add a new function cycle_limit_reached that returns bool, allowing for gracef...Robert Norton
2018-06-27Fix real implementation in C to use GMP rationalsAlasdair Armstrong
2018-06-27RTS: __SetConfig support is off by defaultAlastair Reid
2018-06-27RTS: Add support for __ListConfigAlastair Reid
2018-06-27RTS: Delete __SetConfig stub functionAlastair Reid
2018-06-26turn on warnings when compiling mips c then dial back ones that are triggered...Robert Norton
2018-06-26RTS: implement sleep primitivesAlastair Reid
2018-06-26RTS: stub support for -C command line optionAlastair Reid
2018-06-26ELF: Restore error messages in ELF readerAlastair Reid
2018-06-25Coq: add typeclass based comparison, and instantiate for enumsBrian Campbell
2018-06-25Coq: automatic cast introductionBrian Campbell
2018-06-25Use getopt rather than argp for Mac compatibility in C runtimeAlasdair Armstrong
2018-06-25flush stdout after putchar for terminal emulation purposes.Robert Norton
2018-06-22Precise bitvector subrange functions for Coq.Brian Campbell
2018-06-22Add coq builtins for MIPSBrian Campbell
2018-06-22Coq: library updates, esp extending bitvector multiplies, UndefinedBrian Campbell
2018-06-22Coq: project away range types in comparisonsBrian Campbell
2018-06-21Add command line option support for Sail->C compiled modelsAlasdair Armstrong
2018-06-21Follow Sail2 renaming in Isabelle libraryThomas Bauereiss
2018-06-21Merge branch 'sail2' of github.com:rems-project/sail into sail2Alasdair Armstrong
2018-06-21add PMP registers to CSR, fix buildJon French
2018-06-21Merge branch 'tracing' into sail2Alasdair Armstrong
2018-06-21Fix MIPS wrt changes to C runtimeAlasdair Armstrong
2018-06-21Simplify the ANF->IR translationAlasdair Armstrong
2018-06-20Coq: reverse_endiannessBrian Campbell