aboutsummaryrefslogtreecommitdiffstatshomepage
path: root/validation/scheck/ok.c
diff options
context:
space:
mode:
Diffstat (limited to 'validation/scheck/ok.c')
-rw-r--r--validation/scheck/ok.c6
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