summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2018-07-17Coq: integer shiftsBrian Campbell
2018-07-17Coq: add printing stubsBrian Campbell
2018-07-17Coq: handle E_constraint properlyBrian Campbell
2018-07-16Coq: add support for more complex atom typesBrian Campbell
2018-07-13Merge branch 'sail2' of github.com:rems-project/sail into sail2Brian Campbell
2018-07-12Add missing builtins needed for cheri128 C. Still doesn't build possibly due ...Robert Norton
2018-07-12update arm and mips models for new type of write_ram builtin. Also fix c and ...Robert Norton
2018-07-12Coq: handle all bool conjunctions/disjunctionsBrian Campbell
2018-07-12Coq: remove unnecessary constraint on foreach loopsBrian Campbell
2018-07-11Partially revert change to add_vec_int et alThomas Bauereiss
2018-07-11Fix off-by-one bugs in monomorphisation rewrites involving bitvector subrangesThomas Bauereiss
2018-07-11Fix some signedness bugsThomas Bauereiss
2018-07-10Update HOL setupBrian Campbell
2018-07-10Add more Isabelle lemmas to libraryThomas Bauereiss
2018-07-09Changes for anonymisation. Ensure headers are in correct format. Remove some ...Robert Norton
2018-07-09Update gitignoreThomas Bauereiss
2018-07-09Add some syntactic sugar for IsabelleThomas Bauereiss
2018-07-09Simplify treating of undefined_bool in Lem libraryThomas Bauereiss
2018-07-09Bits for bits of aarch64 in coqBrian Campbell
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:54:26 +0000