diff options
| author | Luc Van Oostenryck <luc.vanoostenryck@gmail.com> | 2021-04-09 18:08:33 +0200 |
|---|---|---|
| committer | Luc Van Oostenryck <luc.vanoostenryck@gmail.com> | 2021-04-13 18:25:43 +0200 |
| commit | 75e72f82c8645db0f8cf6954ce3beb18a00dee37 (patch) | |
| tree | d5f9cc1a416b73f8131cf08fba98bbe773f974bf /validation/scheck | |
| parent | d1ab4c40982ffcfadebf3155f498469aeb1355b0 (diff) | |
| download | sparse-dev-75e72f82c8645db0f8cf6954ce3beb18a00dee37.tar.gz | |
scheck: allow multiple assertions
With the SMT solver used here, by default, once an expression is
checked it's kinda consumed by the process and can't be reused
anymore for another check.
So, enable the incremental mode: it allows to call boolecter_sat()
several times.
Note: Another would be, of course, to just AND together all assertions
and just check this but then we would lost the finer grained
diagnostic in case of failure.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
Diffstat (limited to 'validation/scheck')
| -rw-r--r-- | validation/scheck/ok.c | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c index 76c04c4f..f4a0daab 100644 --- a/validation/scheck/ok.c +++ b/validation/scheck/ok.c @@ -1,10 +1,6 @@ static void ok(int x) { __assert((~x) == (~0 - x)); // true but not simplified yet -} - -static void also_ok(int x) -{ __assert_eq(~x, ~0 - x); } |