Reworks checking of code contracts

This commit completes the work started in the previous commit
by revising the existing contract-handling code into the new pass
--check-code-contracts, which first applies all contracts and then
checks them. By applying the contracts before checking begins, this
checks the relative correctness of each function/loop with respect
to the functions called by/loops contained in it. Since there can
be no infinite sequence of nested functions/loops, these relative
correctness results together imply the correctness of the overall
program. We take this approach rather than checking entirely
without using contracts because it allows significant reuse of
results --- a function that is called many times only needs to be
checked once, and all of its invocations will be abstracted out
by the contract application.

Author: klaas

.gitignore

@@ -19,6 +19,8 @@ src/.settings/*
 # Visual Studio
 Debug/*
 Release/*
+#vi(m)
+*.swp
 
 # compilation files
 *.lo

regression/contracts/function_check_01/test.desc

@@ -1,11 +1,8 @@
 CORE
 main.c
---apply-code-contracts
+--check-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_04/test.desc

@@ -1,11 +1,8 @@
-KNOWNBUG
+CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^\[main.assertion.1\] .* assertion x == 0: SUCCESS$
-^\[foo.1\] line 9 : FAILURE$
+^\[foo.1\] .* : FAILURE$
 ^VERIFICATION FAILED$
 --
 --
---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_mem_01/main.c

@@ -33,7 +33,7 @@ void foo(bar *x)
   __CPROVER_requires(__CPROVER_VALID_MEM(x, sizeof(bar)))
 {
   x->x += 1;
-  return
+  return;
 }
 
 int main()

regression/contracts/function_check_mem_01/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --check-code-contracts
 ^EXIT=0$

regression/contracts/invar_check_01/test.desc

@@ -1,11 +1,8 @@
-KNOWNBUG
+CORE
 main.c
---apply-code-contracts
+--check-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/invar_check_02/test.desc

@@ -1,11 +1,8 @@
-KNOWNBUG
+CORE
 main.c
---apply-code-contracts
+--check-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/invar_check_03/test.desc

@@ -1,11 +1,8 @@
-KNOWNBUG
+CORE
 main.c
---apply-code-contracts
+--check-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/invar_check_04/test.desc

@@ -1,12 +1,11 @@
-KNOWNBUG
+CORE
 main.c
---apply-code-contracts
+--check-code-contracts
+^EXIT=10$
+^SIGNAL=0$
 ^\[main.1\] .* Loop invariant violated before entry: SUCCESS$
 ^\[main.2\] .* Loop invariant not preserved: SUCCESS$
 ^\[main.assertion.1\] .* assertion r == 0: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.