Improve tests.

Author: gebner

examples/dpe/EngineCore.c

@@ -9,7 +9,7 @@
 bool compare(size_t len, const _array uint8_t *a1, const _array uint8_t *a2)
     _requires(a1._length == len)
     _requires(a2._length == len)
-    _ensures((_slprop) _inline_pulse(pure ($(return) <==> Seq.equal (array_value_of $(a1)) (array_value_of $(a2)))))
+    _ensures(return == (bool) _inline_pulse(Seq.equal (array_value_of $(a1)) (array_value_of $(a2))))
 {
     _ghost_stmt(admit());
     return false;

test/complex_arith.c

@@ -1,29 +1,31 @@
 #include "pal.h"
 #include <stdint.h>
 
+_let(bool int_fits(_specint x), INT32_MIN <= x && x <= INT32_MAX)
+
 int triple(int x)
-    _requires((_specint) x * 3 <= INT32_MAX && (_specint) x * 3 >= INT32_MIN)
+    _requires(int_fits((_specint) x * 3))
     _ensures(return == x * 3)
 {
     return x * 3;
 }
 
 int square(int x)
-    _requires((_specint) x * x <= INT32_MAX && (_specint) x * x >= INT32_MIN)
+    _requires(int_fits((_specint) x * x))
     _ensures(return == x * x)
 {
     return x * x;
 }
 
 int double_value(int x)
-    _requires((_specint) x * 2 <= INT32_MAX && (_specint) x * 2 >= INT32_MIN)
+    _requires(int_fits((_specint) x * 2))
     _ensures(return == x * 2)
 {
     return x * 2;
 }
 
 int sum(int x, int y)
-    _requires((_specint) x + y <= INT32_MAX && (_specint) x + y >= INT32_MIN)
+    _requires(int_fits((_specint) x + y))
     _ensures(return == x + y)
 {
     return x + y;