summaryrefslogtreecommitdiff
path: root/lib/vector_dec.sail
AgeCommit message (Expand)Author
2020-04-21Fix sub_bits interpreter bindingThomas Bauereiss
2020-04-21Add more monomorphisation rewritesThomas Bauereiss
2020-02-24Allow overloading of subrange builtins for non-bitvectorsThomas Bauereiss
2019-08-14Use bitvector type in mono rewritesThomas Bauereiss
2019-07-16Merge remote-tracking branch 'origin/sail2' into separate_bvAlasdair Armstrong
2019-06-17Add sail implementation of count_leading_zeros. We could use this for backend...Robert Norton
2019-06-17Implement a count_leading_zeros builtin for ocaml and c. This may be a slight...Robert Norton
2019-06-04Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-05-30Set interpreter builtin for truncateLSB.Robert Norton
2019-05-23Fix bug in slice_maskThomas Bauereiss
2019-05-17Experiment with making vector and bitvector distinct typesAlasdair Armstrong
2019-04-17Add interpreter annots to vector_dec.Prashanth Mundkur
2019-04-15Merge branch 'sail2' into rmem_interpreterJon French
2019-03-18Add non-negative constraints for zeros/onesBrian Campbell
2019-03-15Various monomorphisation tweaks and fixesThomas Bauereiss
2019-03-15Make mono_rewrites less dependant on ASL preludeThomas Bauereiss
2019-02-13Merge branch 'sail2' into rmem_interpreterJon French
2019-02-07Monomorphisation tweaks for v8.5Thomas Bauereiss
2019-02-06Fix some testsAlasdair Armstrong
2018-12-28Merge branch 'sail2' into rmem_interpreterJon French
2018-12-14Add truncateLSB builtin useful for implementing Cheri Concentrate. Also add b...Robert Norton
2018-11-20Add full constraints for vector updatesBrian Campbell
2018-11-19Merge branch 'latex' into sail2Robert Norton
2018-11-19Add missing constraints on bitvector_access, with regression test.Fixes #24.Robert Norton
2018-11-15document signed and unsignedRobert Norton
2018-11-09Improvements to latex generationAlasdair Armstrong
2018-10-24Interpreter: don't silently use OCaml externs, only interpreter externsJon French
2018-07-07Coq: precise generic vectorsBrian Campbell
2018-06-25Coq: automatic cast introductionBrian Campbell
2018-06-22Precise bitvector subrange functions for Coq.Brian Campbell
2018-06-21Merge branch 'tracing' into sail2Alasdair Armstrong
2018-06-19Add elf parsing from AlastairAlasdair Armstrong
2018-06-18Separate bitvector access/update from generic vector access in std preludeBrian Campbell
2018-06-14Refactor C backend, and split RTS into multiple filesAlasdair
2018-06-11actually fix exist_pattern testJon French
2018-06-08Coq: add destructuring of atom existentials in patternsBrian Campbell
2018-06-08Fill in most Coq built-insBrian Campbell
2018-06-07Rename some functions in vector_dec library file to avoid clashes with functi...Robert Norton
2018-05-31Fixes to get ARM u-boot working in Sail.Alasdair Armstrong
2018-05-25Coq: fill in some built-insBrian Campbell
2018-05-23A couple of missing >= 0 constraints on vector handling functionsBrian Campbell
2018-05-09Run ARM built-in tests for Lem backend (via OCaml)Thomas Bauereiss
2018-05-03Work in progress on the coq backendBrian Campbell
2018-04-05Fix precedence printing and update aarch64 specAlasdair Armstrong
2018-02-24Fix C builtinsAlasdair Armstrong
2018-02-23Fix some bugs in C compilationAlasdair Armstrong
2018-02-22More updates to C backendAlasdair Armstrong
2018-02-19Have generic vectors working in C backendAlasdair Armstrong
2018-02-15List support in C backendAlasdair Armstrong
2018-02-13Support for large bitvector literals in C backendAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:01:16 +0000