C library: model currently supported behaviour of longjmp

We require (yet to be built) instrumentation to handle longjmp (and its
variants). Therefore:

1) The only possible return value of `setjmp` (and its variants) is 0
for it can never be reached via longjmp (or its variants).
2) Fail an assertion when invoking longjmp to ensure we do not produce
unsound verification results when longjmp is reachable on some path.

Enable all related regression tests.

Author: tautschnig

regression/cbmc-library/_longjmp-01/main.c

@@ -1,9 +1,10 @@
-#include <assert.h>
 #include <setjmp.h>
 
+static jmp_buf env;
+
 int main()
 {
-  _longjmp();
-  assert(0);
+  _longjmp(env, 1);
+  __CPROVER_assert(0, "unreachable");
   return 0;
 }

regression/cbmc-library/_longjmp-01/test.desc

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
-^EXIT=0$
+^\[_longjmp.assertion.1\] line 12 _longjmp requires instrumentation: FAILURE$
+^\[main.assertion.1\] line 8 unreachable: SUCCESS$
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc-library/longjmp-01/main.c

@@ -1,9 +1,10 @@
-#include <assert.h>
 #include <setjmp.h>
 
+static jmp_buf env;
+
 int main()
 {
-  longjmp();
-  assert(0);
+  longjmp(env, 1);
+  __CPROVER_assert(0, "unreachable");
   return 0;
 }

regression/cbmc-library/longjmp-01/test.desc

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
-^EXIT=0$
+^\[longjmp.assertion.1\] line 12 longjmp requires instrumentation: FAILURE$
+^\[main.assertion.1\] line 8 unreachable: SUCCESS$
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc-library/setjmp-01/main.c

@@ -1,9 +1,12 @@
-#include <assert.h>
 #include <setjmp.h>
 
+static jmp_buf env;
+
 int main()
 {
-  setjmp();
-  assert(0);
+  if(setjmp(env))
+    __CPROVER_assert(0, "reached via longjmp");
+  else
+    __CPROVER_assert(0, "setjmp called directly");
   return 0;
 }

regression/cbmc-library/setjmp-01/test.desc

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
-^EXIT=0$
+^\[main.assertion.1\] line 8 reached via longjmp: SUCCESS$
+^\[main.assertion.2\] line 10 setjmp called directly: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc-library/siglongjmp-01/main.c

@@ -1,9 +1,10 @@
-#include <assert.h>
 #include <setjmp.h>
 
+static sigjmp_buf env;
+
 int main()
 {
-  siglongjmp();
-  assert(0);
+  siglongjmp(env, 1);
+  __CPROVER_assert(0, "unreachable");
   return 0;
 }

regression/cbmc-library/siglongjmp-01/test.desc

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE unix
 main.c
 --pointer-check --bounds-check
-^EXIT=0$
+^\[siglongjmp.assertion.1\] line 14 siglongjmp requires instrumentation: FAILURE$
+^\[main.assertion.1\] line 8 unreachable: SUCCESS$
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc-library/sigsetjmp-01/main.c

@@ -0,0 +1,12 @@
+#include <setjmp.h>
+
+static sigjmp_buf env;
+
+int main()
+{
+  if(sigsetjmp(env, 0))
+    __CPROVER_assert(0, "reached via siglongjmp");
+  else
+    __CPROVER_assert(0, "sigsetjmp called directly");
+  return 0;
+}

regression/cbmc-library/sigsetjmp-01/test.desc

@@ -0,0 +1,10 @@
+CORE unix
+main.c
+--pointer-check --bounds-check
+^\[main.assertion.1\] line 8 reached via siglongjmp: SUCCESS$
+^\[main.assertion.2\] line 10 sigsetjmp called directly: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring