diff options
| author | Luc Van Oostenryck <luc.vanoostenryck@gmail.com> | 2021-04-09 23:36:32 +0200 |
|---|---|---|
| committer | Luc Van Oostenryck <luc.vanoostenryck@gmail.com> | 2021-04-13 18:25:43 +0200 |
| commit | 2e3c2464ca3522fe0a6dfc93ea36c88cbe7bf117 (patch) | |
| tree | bad98ff1c69a4e53c17324844c01771627a6d889 /validation/scheck | |
| parent | 0b0805cf17aeb6a6cd0a7ed3f47ad8f0b4a3407b (diff) | |
| download | sparse-dev-2e3c2464ca3522fe0a6dfc93ea36c88cbe7bf117.tar.gz | |
scheck: support pre-conditions via __assume()
A lot of simplifications are only valid when their variables
satisfy to some conditions (like "is within a given range" or
"is a power of two").
So, allow to add such pre-conditions via new _assume() statements.
Internally, all such preconditions are ANDed together and what is
checked is they imply the assertions:
AND(pre-condition) implies assertion 1
...
Note: IIUC, it seems that boolector has a native mechanism for such
things but I'm not sure if t can be used here.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
Diffstat (limited to 'validation/scheck')
| -rw-r--r-- | validation/scheck/ok.c | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c index 8f65013e..1e5314f2 100644 --- a/validation/scheck/ok.c +++ b/validation/scheck/ok.c @@ -10,6 +10,12 @@ static void always(int x) __assert((x - x) == 0); // true and simplified } +static void assumed(int x, int a, int b) +{ + __assume((a & ~b) == 0); + __assert_eq((x ^ a) | b, x | b); +} + /* * check-name: scheck-ok * check-command: scheck $file |