summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Collapse)Author
2019-12-01Coq: remove last use and definition of doc_nc_propBrian Campbell
(plus test, as it wasn't covered before)
2019-11-11Make sure undefined_gen inserts enough type annotations for union constructorsAlasdair Armstrong
2019-11-07Make the world a slightly more sane and consistent placeAlasdair Armstrong
2019-11-07Backport fixes to SMT generation from poly_mapping branchAlasdair Armstrong
2019-11-05Forbid types declared after a scattered union being used in clausesAlasdair
The following is therefore always forbidden ``` scattered union U enum E = A | B | C union clause U = Ctor : E ``` We attempt to detect when this occurs and include a hint indicating the likely reason why a 'Undefined type E' error might occur in this circumstance
2019-11-05Improve type error for recursive types slightlyAlasdair Armstrong
2019-11-05Make sure we correctly forbid recursive datatypes that we don't want to supportAlasdair Armstrong
Ensure we give a nice error message that explains that recursive types are forbidden ``` Type error: [struct_rec.sail]:3:10-11 3 | field : S | ^ | Undefined type S | This error was caused by: | [struct_rec.sail]:2:0-4:1 | 2 |struct S = { | |^----------- | 4 |} | |^ | | Recursive types are not allowed ``` The theorem prover backends create a special register_value union that can be recursive, so we make sure to special case that.
2019-11-04Some almost-forgotten mono testsBrian Campbell
2019-11-01Add a missing well-formedness checkAlasdair
2019-10-02Coq: limited support for existentially-typed tuplesBrian Campbell
- in particular at monadic interfaces (i.e., sufficient for instruction ast types) - see commented out part of test/coq/pass/ast_with_dep_tuple.sail for an example that's not currently supported - generate definitions for type-level Bool definitions (i.e., predicates)
2019-09-02Enable part of a test that's been fixed recently.Brian Campbell
2019-08-30Add a couple of overlooked testsBrian Campbell
2019-08-29Clean up some mono testsBrian Campbell
2019-08-14Update testsThomas Bauereiss
2019-08-02Fix up some edge cases with the bitvector/polyvector splitBrian Campbell
Mostly in the Coq backend, plus a few testcases that use bitvector builtins on poly-vectors (which works on some backends, but not Coq). Also handle some additional list inclusion proofs in Coq.
2019-08-01Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-08-01Merge remote-tracking branch 'origin/rv_duopod_fix' into sail2Alasdair Armstrong
Fixes #53
2019-07-31Fix failing SMT testAlasdair Armstrong
2019-07-31Remove redundant ifdef and run SMT tests by defaultAlasdair Armstrong
2019-07-18Add a feature flag for barrier type changeAlasdair Armstrong
Fix SMT mem_builtin test case
2019-07-17Add another test caseAlasdair Armstrong
2019-07-16Fix all remaining tests for this branchAlasdair
2019-07-16Get monomorphisation tests working with separate bitvectorsAlasdair Armstrong
2019-07-16Merge remote-tracking branch 'origin/sail2' into separate_bvAlasdair Armstrong
2019-06-30Fix bug with toplevel pattern in RISC-V duopodAlasdair
Do this by making sure that generic pattern literal re-writing gets applied to top-level function clauses. This requires re-ordering the rewrites for most backends otherwise they break, which hopefully wo anything. After doing this re-ordering I had to turn off casting when rewriting bitvector patterns, otherwise insane things can happen.
2019-06-27SMT: Add a reverse endianness function and fix some bugsAlasdair Armstrong
2019-06-25SMT: Add another case to appendAlasdair Armstrong
2019-06-21Coq: add missing property derivation casts for effectful expressionsBrian Campbell
These don't appear much, but are now showing up in the sail-arm model due to an innocent change elsewhere.
2019-06-21Coq: be more careful when dealing with wildcard argument patternsBrian Campbell
If they're merged with a type variable then we still need to name the argument so that it can be used in other types.
2019-06-20Handle more uses of mutable variables during monomorphisation cast insertionBrian Campbell
In particular, bitvector subrange updates work with this version.
2019-06-19Make C emulator exit with failure for uncaught exception. Make special case ↵Robert Norton
for 'exception.sail' test that deliberately exits with uncaught exception.
2019-06-19Monomorphisation improvements for aarch64_smallBrian Campbell
- additional rewrites (signed extend of subrange@zeros, subrange assignment, variants with casts) - drop # from new top-level type variables (e.g., n_times_8) so that the rewriter knows that they're safe to include in casts - add casts in else-branches when only one possible value for a size is left - add casts when assertions force a size to be a particular value - don't use types to detect set constraints in analysis because we won't know which part of the assertion should be replaced - also use non-top-level type variables when simplifying sizes in analysis (useful when it can from pattern matching on an ast) - cope with repeated int('n) in a pattern match (!)
2019-06-18Fix two SMT test casesThomas Bauereiss
2019-06-18Update test casesThomas Bauereiss
2019-06-18Implement count_leading_zeros in LemThomas Bauereiss
2019-06-17Implement a count_leading_zeros builtin for ocaml and c. This may be a ↵Robert Norton
slight performance improvement and keeps compatibility with smt backend that already had a builtin for this because it can't handle the loop in the sail version. Will need implementations for prover backends.
2019-06-10Add well-formedness check for type schemes in valspecs.Brian Campbell
Fixes #47. Also adjust the nexp substitution so that the error message points to a useful location, and replace the empty environment with the initial environment in a few functions that do type checking to ensure that the prover is set up (which may be needed for the wf check).
2019-06-06Fix aarch64_small testAlasdair Armstrong
2019-06-06Add arith_shiftr to C and OCaml librariesThomas Bauereiss
2019-06-05Add some regression testsAlasdair
2019-06-04Make sure aarch64_small can generate Jib for SMTAlasdair Armstrong
Add a test case for this
2019-06-04Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-06-04SMT: Add a fuzzing tool for the SMT builtinsAlasdair Armstrong
2019-06-03Test case for previous commitBrian Campbell
2019-05-29SMT: Make bitvector equality work between vectors of different lengthsAlasdair Armstrong
2019-05-29SMT: Fix sail_truncate and sail_mask for unusual argument typesAlasdair Armstrong
2019-05-28Fix typechecking test expected errorAlasdair Armstrong
2019-05-28Just build lem in aarch64_small testAlasdair Armstrong
2019-05-28SMT: Add min and max functionsAlasdair Armstrong
Allow conversion between int(n) and int in smt_conversion
2019-05-28Make sure single clause functions with top-level guards work correctlyAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 12:54:28 +0000