Merge pull request #2309 from qaphla/regression

Regression tests for code contracts

Author: tautschnig

regression/Makefile

@@ -18,7 +18,8 @@ DIRS = cbmc \
        goto-cc-cbmc \
        cbmc-cpp \
        goto-cc-goto-analyzer \
-       systemc
+       systemc \
+       contracts \
        # Empty last line
 
 # Tests under goto-gcc cannot be run on Windows, so appveyor.yml unlinks

regression/contracts/CMakeLists.txt

@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}"
+)

regression/contracts/Makefile

@@ -0,0 +1,35 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows=true
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows=false
+endif
+
+test:
+	@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
+
+tests.log:
+	@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/contracts/chain.sh

@@ -0,0 +1,38 @@
+#!/bin/bash
+
+set -e
+
+goto_cc=$1
+goto_instrument=$2
+cbmc=$3
+is_windows=$4
+
+name=${*:$#}
+name=${name%.c}
+
+args=${*:5:$#-5}
+
+if [[ "${is_windows}" == "true" ]]; then
+  $goto_cc "${name}.c"
+  mv "${name}.exe" "${name}.gb"
+else
+  $goto_cc -o "${name}.gb" "${name}.c"
+fi
+
+$goto_instrument ${args} "${name}.gb" "${name}-mod.gb"
+if [ ! -e "${name}-mod.gb" ] ; then
+  cp "$name.gb" "${name}-mod.gb"
+elif echo $args | grep -q -- "--dump-c" ; then
+  mv "${name}-mod.gb" "${name}-mod.c"
+
+  if [[ "${is_windows}" == "true" ]]; then
+    $goto_cc "${name}-mod.c"
+    mv "${name}-mod.exe" "${name}-mod.gb"
+  else
+    $goto_cc -o "${name}-mod.gb" "${name}-mod.c"
+  fi
+
+  rm "${name}-mod.c"
+fi
+$goto_instrument --show-goto-functions "${name}-mod.gb"
+$cbmc "${name}-mod.gb"

regression/contracts/function_apply_01/main.c

@@ -0,0 +1,20 @@
+// function_apply_01
+
+// Note that this test is supposed to have an incorrect contract.
+// We verify that applying (without checking) the contract yields success,
+// and that checking the contract yields failure.
+
+#include <assert.h>
+
+int foo() 
+  __CPROVER_ensures(__CPROVER_return_value == 0)
+{
+  return 1;
+}
+
+int main()
+{
+  int x = foo();
+  assert(x == 0);
+  return 0;
+}

regression/contracts/function_apply_01/test.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+main.c
+--apply-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Applying code contracts currently also checks them.

regression/contracts/function_check_01/main.c

@@ -0,0 +1,31 @@
+// function_check_01
+
+// This tests a simple example of a function with requires and
+// ensures which should both be satisfied.
+
+#include <assert.h>
+
+int min(int a, int b)
+  __CPROVER_requires(a >= 0 && b >= 0)
+  __CPROVER_ensures(__CPROVER_return_value <= a &&
+                    __CPROVER_return_value <= b &&
+                   (__CPROVER_return_value == a || __CPROVER_return_value == b)
+                   )
+{
+  if(a <= b)
+  {
+    return a;
+  }
+  else
+  {
+    return b;
+  }
+}
+
+int main()
+{
+  int x, y, z;
+  __CPROVER_assume(x >= 0 && y >= 0);
+  z = min(x, y);
+  assert(z <= x);
+}

regression/contracts/function_check_01/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+--check-code-contracts not implemented yet.
+--apply-code-contracts is the current name for the flag. This should be
+updated as the flag changes.

regression/contracts/function_check_02/main.c

@@ -0,0 +1,24 @@
+// function_check_02
+
+// This test checks the use of quantifiers in ensures clauses.
+// A known bug (resolved in PR #2278) causes the use of quantifiers
+// in ensures to fail.
+
+int initialize(int *arr)
+  __CPROVER_ensures(
+    __CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == i}
+  )
+{
+  for(int i = 0; i < 10; i++)
+  {
+    arr[i] = i;
+  }
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  initialize(arr);
+}

regression/contracts/function_check_02/test.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--check-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Ensures statements currently do not allow quantified predicates unless the
+function has void return type.