3 files changed, 38 insertions, 0 deletions
diff --git a/validation/scheck/ko.c b/validation/scheck/ko.c
new file mode 100644
index 00000000..dbd861ea
--- /dev/null
+++ b/validation/scheck/ko.c
@@ -0,0 +1,10 @@
+static void ko(int x)
+{
+	__assert((~x) == (~0 + x));
+}
+
+/*
+ * check-name: scheck-ko
+ * check-command: scheck $file
+ * check-known-to-fail
+ */
diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c
new file mode 100644
index 00000000..1e5314f2
--- /dev/null
+++ b/validation/scheck/ok.c
@@ -0,0 +1,22 @@
+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)
+{
+	__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
+ */
diff --git a/validation/test-suite b/validation/test-suite
index 370cd35a..305edd1f 100755
--- a/validation/test-suite
+++ b/validation/test-suite
@@ -13,6 +13,9 @@ prog_name=`basename $0`
 if [ ! -x "$default_path/sparse-llvm" ]; then
 	disabled_cmds="sparsec sparsei sparse-llvm sparse-llvm-dis"
 fi
+if [ ! -x "$default_path/scheck" ]; then
+	disabled_cmds="$disabled_cmds scheck"
+fi
 
 # flags:
 #	- some tests gave an unexpected result
@@ -514,6 +517,7 @@ echo "    -f                         write a test known to fail"
 echo "    -l                         write a test for linearized code"
 echo "    -r                         write a test for linearized code returning 1"
 echo "    -p                         write a test for pre-processing"
+echo "    -s                         write a test for symbolic checking"
 echo
 echo "argument(s):"
 echo "    file                       file containing the test case(s)"
@@ -545,6 +549,8 @@ do_format()
 			ret=1 ;;
 		-p)
 			def_cmd='sparse -E $file' ;;
+		-s)
+			def_cmd='scheck $file' ;;
 
 		help|-*)
 			do_format_help