diff options
| author | Luc Van Oostenryck <luc.vanoostenryck@gmail.com> | 2021-04-09 18:10:44 +0200 |
|---|---|---|
| committer | Luc Van Oostenryck <luc.vanoostenryck@gmail.com> | 2021-04-13 18:25:43 +0200 |
| commit | 0b0805cf17aeb6a6cd0a7ed3f47ad8f0b4a3407b (patch) | |
| tree | dd8b12f16d1b03c88ecca62e0d97a82bda389261 /validation | |
| parent | 75e72f82c8645db0f8cf6954ce3beb18a00dee37 (diff) | |
| download | sparse-dev-0b0805cf17aeb6a6cd0a7ed3f47ad8f0b4a3407b.tar.gz | |
scheck: assert_const()
Since, the symbolic checker check expressions at the ... symbolic
level, this can be used to check if two expressions are equivalent
but not if this equivalence is effectively used.
So, add a new assertion (this time not at the symbolic level) to
check if an expression which is expected to simplify to a constant
is effectively simplified to this constant.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
Diffstat (limited to 'validation')
| -rw-r--r-- | validation/scheck/ok.c | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c index f4a0daab..8f65013e 100644 --- a/validation/scheck/ok.c +++ b/validation/scheck/ok.c @@ -2,6 +2,7 @@ static void ok(int x) { __assert((~x) == (~0 - x)); // true but not simplified yet __assert_eq(~x, ~0 - x); + __assert_const(x & 0, 0); } static void always(int x) |