summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
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
2018-06-20Coq: Tidy up libraries, export StringBrian Campbell
2018-06-20Coq: port handling of effectful and/or from Lem backendBrian Campbell
2018-06-20Coq: a few more opsBrian 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-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-15Fixes for C RTS for aarch64 no it's split into multiple filesAlasdair Armstrong
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: support for range type, along with related existential improvementsBrian Campbell
2018-06-12Coq: add more to libraryBrian Campbell
2018-06-11More efficient bitfield implementationAlasdair Armstrong
2018-06-11actually fix exist_pattern testJon 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-08Coq: add destructuring of atom existentials in patternsBrian Campbell
2018-06-08Coq: existential and constraint solving workBrian Campbell
2018-06-08Coq: some very basic existential supportBrian Campbell
2018-06-08Fill in most Coq built-insBrian Campbell
2018-06-08Add missing Coq builtin info to vector_incBrian Campbell
2018-06-07Fix bug in add_bits optimizationAlasdair Armstrong
2018-06-07Rename some functions in vector_dec library file to avoid clashes with functi...Robert Norton
2018-06-07Fixes and additions to c builtins needed to pass mips test suite. bv_ts shoul...Robert Norton
2018-06-04Update sail C libraryAlasdair Armstrong
2018-05-31Fixes to get ARM u-boot working in Sail.Alasdair Armstrong
2018-05-31Add auxiliary script to HolmakefileRamana Kumar
2018-05-31Add some HOL4 termination proofs for state.lemRamana Kumar
2018-05-25Coq: fill in some built-insBrian Campbell
2018-05-25allow loading multiple raw files in ocaml main backend to allow kernel and dt...Robert Norton
2018-05-24Coq: solve more constraintsBrian Campbell
2018-05-24Help launch coqideBrian Campbell
2018-05-24Import (rather hacky) Coq Sail librariesBrian Campbell
2018-05-23A couple of missing >= 0 constraints on vector handling functionsBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:25:13 +0000