diff options
| author | Alasdair Armstrong | 2018-12-12 17:37:13 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-12-12 17:47:55 +0000 |
| commit | 56fb5bf999d7cc900d6535da4168e220862d3d9c (patch) | |
| tree | 4dd0c0a3926c1cc10c39e94f00e7473acc1af0d1 /editors | |
| parent | 54914eff75322309ad6505905c24806f3c7396f3 (diff) | |
Add a test case for various simple boolean properties
test/typecheck/pass/tautology.sail constaints tests of various boolean
properties, e.g.
// de Morgan
_prove(constraint(not('p | 'q) <--> not('p) & not('q)));
_prove(constraint(not('p & 'q) <--> not('p) | not('q)));
introduce a new _not_prove case which allows us to assert in tests
that a constraint is not provable. This test essentially tests that
constraints map to sensible problems in the SMT solver, without
testing flow typing or any other features.
Add a script test/typecheck/update_errors.sh, which regenerates the
expected error messages. Testing that type-checking failures is
important, but can be brittle when the error messages change for
inconsequential reasons. This script automates fixing this.
Also ensure that this test case works correctly in Lem
Diffstat (limited to 'editors')
| -rw-r--r-- | editors/sail2-mode.el | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el index b7998357..38404f14 100644 --- a/editors/sail2-mode.el +++ b/editors/sail2-mode.el @@ -21,7 +21,7 @@ "uint64_t" "int64_t" "bv_t" "mpz_t")) (defconst sail2-special - '("_prove" "create" "kill" "convert" "undefined" + '("_prove" "_not_prove" "create" "kill" "convert" "undefined" "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif" "$option" "$latex")) (defconst sail2-font-lock-keywords |