summaryrefslogtreecommitdiff
path: root/lib
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-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
2018-05-18Make named theorem collections of state monad more fine-grainedThomas Bauereiss
2018-05-18Add lemmas about monadic Boolean connectivesThomas Bauereiss
2018-05-18use correct inequality for strings.Robert Norton
2018-05-18Add sail_valuesAuxiliary rw theorems to computeLibRamana Kumar
2018-05-18Improve sail-heap dependencies in the HolmakefileRamana Kumar
2018-05-18Avoid split_on_char function that was introduced in OCaml 4.04. Use Util vers...Robert Norton
2018-05-17changes to for testing FreeBSD boot on MIPS: allowing loading raw file in oca...Robert Norton
2018-05-17Merge branch 'cheri-mono' into sail2Brian Campbell
2018-05-17Clean up MIPS for HOL4 a littleBrian Campbell
2018-05-17Use an intermediate base_monad type alias in Lem,Brian Campbell
2018-05-16Add handwritten script to HolmakefileBrian Campbell
2018-05-16More targeted gitignore for HOL4Brian Campbell
2018-05-16Termination proofs and lemmata for sail_values holRamana Kumar
2018-05-15Merge branch 'sail2' into mappingsJon French
2018-05-15Make all of Sail HOL libraries, not just the base heapBrian Campbell
2018-05-11Add snapshot of generated Isabelle theoriesThomas Bauereiss
2018-05-11Merge branch 'sail2' into cheri-monoThomas Bauereiss
2018-05-10RISC-V in HOL4Brian Campbell
2018-05-10Clean up HOL library properlyBrian Campbell
2018-05-10Merge branch 'sail2' into mappingsJon French
2018-05-09Fix an issue with C compilationAlasdair Armstrong
2018-05-09Add tests for Isabelle->OCaml generation for CHERI and AArch64Thomas Bauereiss
2018-05-09Run ARM built-in tests for Lem backend (via OCaml)Thomas Bauereiss
2018-05-07HOL script generation for library and CHERIBrian Campbell
2018-05-04Add back purely sequential Lem generationThomas Bauereiss
2018-05-03Flow typing and l-expression changes for ASL parserAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:08:56 +0000