summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2018-07-09Update CHERI code generation from IsabelleThomas Bauereiss
2018-07-09Simplify treating of undefined_bool in Lem libraryThomas Bauereiss
2018-07-07Add the lrsc tests from riscv-tests.Prashanth Mundkur
2018-07-07Coq: bbv have reorganised their repositoryBrian Campbell
2018-07-05Fix equality comparisons for structsAlasdair
2018-07-05Fix CHERI test that was failing when compiled to CAlasdair Armstrong
2018-07-03Fix a bug in foreach loopsAlasdair Armstrong
2018-06-30Fix an issue with vector_update_subrangeAlasdair
2018-06-27Actually fix real literals, and add a test for various propertiesAlasdair Armstrong
2018-06-27Fix reading reals from strings in C libAlasdair Armstrong
2018-06-26In guarded pattern rewriting, irrefutable patterns subsume wildcardsBrian Campbell
2018-06-22Fix up constraints in OCaml reg_ref testBrian Campbell
2018-06-22build mips and mips_c when running tests.Robert Norton
2018-06-21Merge branch 'tracing' into sail2Alasdair Armstrong
2018-06-21Simplify the ANF->IR translationAlasdair Armstrong
2018-06-18Mono test script updateBrian 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-12Coq: support for range type, along with related existential improvementsBrian Campbell
2018-06-12Prove test_raw_add theorem for init_stateRamana Kumar
2018-06-12Make progress on HOL4 test_raw_addRamana Kumar
2018-06-12Work on HOL symbolic evaluation of installing codeRamana Kumar
2018-06-12Experimentation with PrePost for test_raw_addRamana Kumar
2018-06-12Speculation on executing a CHERI test in HOL4Ramana Kumar
2018-06-11actually fix exist_pattern testJon French
2018-06-11fix test exist_pattern.sail -- lem needed much more of the stdlib to be importedJon French
2018-06-11Merge branch 'sail2' into mappingsJon French
2018-06-11ocaml test prelude: option is now in stdlibJon French
2018-06-09Fix issue in C_backend, and run C tests with undefined behavior sanitizerAlasdair
2018-06-09Fix issue with catch block return values not being compiled correctlyAlasdair
2018-06-08Coq: add destructuring of atom existentials in patternsBrian Campbell
2018-06-08Coq: ignore some currently unsupported testsBrian Campbell
2018-06-08Coq: skip two tests with redundant pattern matchesBrian Campbell
2018-06-07Rename some functions in vector_dec library file to avoid clashes with functi...Robert Norton
2018-06-06Some additional fixes to C backend. Re-enable primitive optimizations.Alasdair Armstrong
2018-06-06Some work on improving error messagesAlasdair Armstrong
2018-06-04Fix an issue with riscv_platform involving flow typingAlasdair Armstrong
2018-05-31Fixes to get ARM u-boot working in Sail.Alasdair Armstrong
2018-05-28Coq: add back tests with undefined functionsBrian Campbell
2018-05-28Coq: add option to produce axioms for unimplemented functionsBrian Campbell
2018-05-24Revert "Allow instantiation of type or order type variables without kind decl...Brian 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-22Fix one part of cast introduction, leave another for laterBrian Campbell
2018-05-22Re-enable the RISC-V lem build, and switch the test-suite to use the platform...Prashanth Mundkur
2018-05-17Merge branch 'cheri-mono' into sail2Brian Campbell
2018-05-17Clean out old sequential filesBrian Campbell
2018-05-17Fix Isabelle->OCaml wrapperThomas Bauereiss
2018-05-15Merge branch 'sail2' into mappingsJon French
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:54:30 +0000