index
:
sail
sail2
Formal specification language for ISAs
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test
Age
Commit message (
Expand
)
Author
2018-06-27
Actually fix real literals, and add a test for various properties
Alasdair Armstrong
2018-06-27
Fix reading reals from strings in C lib
Alasdair Armstrong
2018-06-26
In guarded pattern rewriting, irrefutable patterns subsume wildcards
Brian Campbell
2018-06-22
Fix up constraints in OCaml reg_ref test
Brian Campbell
2018-06-22
build mips and mips_c when running tests.
Robert Norton
2018-06-21
Merge branch 'tracing' into sail2
Alasdair Armstrong
2018-06-21
Simplify the ANF->IR translation
Alasdair Armstrong
2018-06-18
Mono test script update
Brian Campbell
2018-06-15
Fixes for C RTS for aarch64 no it's split into multiple files
Alasdair Armstrong
2018-06-14
Refactor C backend, and split RTS into multiple files
Alasdair
2018-06-13
Tracing instrumentation for C backend
Alasdair Armstrong
2018-06-12
Coq: support for range type, along with related existential improvements
Brian Campbell
2018-06-12
Prove test_raw_add theorem for init_state
Ramana Kumar
2018-06-12
Make progress on HOL4 test_raw_add
Ramana Kumar
2018-06-12
Work on HOL symbolic evaluation of installing code
Ramana Kumar
2018-06-12
Experimentation with PrePost for test_raw_add
Ramana Kumar
2018-06-12
Speculation on executing a CHERI test in HOL4
Ramana Kumar
2018-06-11
actually fix exist_pattern test
Jon French
2018-06-11
fix test exist_pattern.sail -- lem needed much more of the stdlib to be imported
Jon French
2018-06-11
Merge branch 'sail2' into mappings
Jon French
2018-06-11
ocaml test prelude: option is now in stdlib
Jon French
2018-06-09
Fix issue in C_backend, and run C tests with undefined behavior sanitizer
Alasdair
2018-06-09
Fix issue with catch block return values not being compiled correctly
Alasdair
2018-06-08
Coq: add destructuring of atom existentials in patterns
Brian Campbell
2018-06-08
Coq: ignore some currently unsupported tests
Brian Campbell
2018-06-08
Coq: skip two tests with redundant pattern matches
Brian Campbell
2018-06-07
Rename some functions in vector_dec library file to avoid clashes with functi...
Robert Norton
2018-06-06
Some additional fixes to C backend. Re-enable primitive optimizations.
Alasdair Armstrong
2018-06-06
Some work on improving error messages
Alasdair Armstrong
2018-06-04
Fix an issue with riscv_platform involving flow typing
Alasdair Armstrong
2018-05-31
Fixes to get ARM u-boot working in Sail.
Alasdair Armstrong
2018-05-28
Coq: add back tests with undefined functions
Brian Campbell
2018-05-28
Coq: add option to produce axioms for unimplemented functions
Brian Campbell
2018-05-24
Revert "Allow instantiation of type or order type variables without kind decl...
Brian Campbell
2018-05-24
Import (rather hacky) Coq Sail libraries
Brian Campbell
2018-05-23
A couple of missing >= 0 constraints on vector handling functions
Brian Campbell
2018-05-22
Fix one part of cast introduction, leave another for later
Brian Campbell
2018-05-22
Re-enable the RISC-V lem build, and switch the test-suite to use the platform...
Prashanth Mundkur
2018-05-17
Merge branch 'cheri-mono' into sail2
Brian Campbell
2018-05-17
Clean out old sequential files
Brian Campbell
2018-05-17
Fix Isabelle->OCaml wrapper
Thomas Bauereiss
2018-05-15
Merge branch 'sail2' into mappings
Jon French
2018-05-14
import new build of riscv tests including some new ones that are expected to ...
Robert Norton
2018-05-12
Fix bug in handling of registers with option type
Thomas Bauereiss
2018-05-11
Add Isabelle code generation for sequential CHERI model
Thomas Bauereiss
2018-05-10
Merge branch 'sail2' into mappings
Jon French
2018-05-09
Adapt Isabelle code generation to Byte_sequence changes
Thomas Bauereiss
2018-05-09
Add tests for Isabelle->OCaml generation for CHERI and AArch64
Thomas Bauereiss
2018-05-09
Run ARM built-in tests for Lem backend (via OCaml)
Thomas Bauereiss
2018-05-08
fixed sub-mappings
Jon French
[next]