summaryrefslogtreecommitdiff
path: root/lib/vector_inc.sail
AgeCommit message (Expand)Author
2020-02-24Allow overloading of subrange builtins for non-bitvectorsThomas Bauereiss
2019-05-17Experiment with making vector and bitvector distinct typesAlasdair Armstrong
2018-12-28Merge branch 'sail2' into rmem_interpreterJon French
2018-11-20Add full constraints for vector updatesBrian Campbell
2018-11-19Add missing constraints on bitvector_access, with regression test.Fixes #24.Robert Norton
2018-10-24Interpreter: don't silently use OCaml externs, only interpreter externsJon French
2018-06-25Coq: automatic cast introductionBrian Campbell
2018-06-22Precise bitvector subrange functions for Coq.Brian Campbell
2018-06-18Separate bitvector access/update from generic vector access in std preludeBrian Campbell
2018-06-08Fill in most Coq built-insBrian Campbell
2018-06-08Add missing Coq builtin info to vector_incBrian Campbell
2018-05-25Coq: fill in some built-insBrian Campbell
2018-05-23A couple of missing >= 0 constraints on vector handling functionsBrian Campbell
2018-04-05Add generic prelude library that pulls in various basic sailAlasdair Armstrong