aboutsummaryrefslogtreecommitdiffstatshomepage
path: root/validation
diff options
Diffstat (limited to 'validation')
-rw-r--r--validation/scheck/ko.c10
-rw-r--r--validation/scheck/ok.c14
-rwxr-xr-xvalidation/test-suite6
3 files changed, 30 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..113912e0
--- /dev/null
+++ b/validation/scheck/ok.c
@@ -0,0 +1,14 @@
+static void ok(int x)
+{
+ __assert((~x) == (~0 - x)); // true but not simplified yet
+}
+
+static void always(int x)
+{
+ __assert((x - x) == 0); // true and simplified
+}
+
+/*
+ * check-name: scheck-ok
+ * check-command: scheck $file
+ */
diff --git a/validation/test-suite b/validation/test-suite
index 1b05c75e..2f7950ef 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
@@ -513,6 +516,7 @@ echo " -a append the created test to the input file"
echo " -f write a test known to fail"
echo " -l write a test for linearized code"
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)"
@@ -540,6 +544,8 @@ do_format()
linear=1 ;;
-p)
def_cmd='sparse -E $file' ;;
+ -s)
+ def_cmd='scheck $file' ;;
help|-*)
do_format_help