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

src/ansi-c/library/setjmp.c

@@ -11,6 +11,7 @@ inline void longjmp(jmp_buf env, int val)
   // does not return
   (void)env;
   (void)val;
+  __CPROVER_assert(0, "longjmp requires instrumentation");
   __CPROVER_assume(0);
 }
 
@@ -26,11 +27,14 @@ inline void _longjmp(jmp_buf env, int val)
   // does not return
   (void)env;
   (void)val;
+  __CPROVER_assert(0, "_longjmp requires instrumentation");
   __CPROVER_assume(0);
 }
 
 /* FUNCTION: siglongjmp */
 
+#ifndef _WIN32
+
 #ifndef __CPROVER_SETJMP_H_INCLUDED
 #include <setjmp.h>
 #define __CPROVER_SETJMP_H_INCLUDED
@@ -41,22 +45,82 @@ inline void siglongjmp(sigjmp_buf env, int val)
   // does not return
   (void)env;
   (void)val;
+  __CPROVER_assert(0, "siglongjmp requires instrumentation");
   __CPROVER_assume(0);
 }
 
+#endif
+
 /* FUNCTION: setjmp */
 
 #ifndef __CPROVER_SETJMP_H_INCLUDED
 #include <setjmp.h>
 #define __CPROVER_SETJMP_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+#undef setjmp
 
 inline int setjmp(jmp_buf env)
 {
-  // store PC
-  int retval=__VERIFIER_nondet_int();
   (void)env;
-  return retval;
+  // returns via longjmp require instrumentation; only such returns would
+  // return a non-zero value
+  return 0;
+}
+
+/* FUNCTION: _setjmp */
+
+#ifndef __CPROVER_SETJMP_H_INCLUDED
+#include <setjmp.h>
+#define __CPROVER_SETJMP_H_INCLUDED
+#endif
+
+inline int _setjmp(jmp_buf env)
+{
+  (void)env;
+  // returns via longjmp require instrumentation; only such returns would
+  // return a non-zero value
+  return 0;
+}
+
+/* FUNCTION: sigsetjmp */
+
+#ifndef _WIN32
+
+#ifndef __CPROVER_SETJMP_H_INCLUDED
+#  include <setjmp.h>
+#  define __CPROVER_SETJMP_H_INCLUDED
+#endif
+
+#undef sigsetjmp
+
+inline int sigsetjmp(sigjmp_buf env, int savesigs)
+{
+  (void)env;
+  (void)savesigs;
+  // returns via siglongjmp require instrumentation; only such returns would
+  // return a non-zero value
+  return 0;
+}
+
+#endif
+
+/* FUNCTION: __sigsetjmp */
+
+#ifndef _WIN32
+
+#ifndef __CPROVER_SETJMP_H_INCLUDED
+#  include <setjmp.h>
+#  define __CPROVER_SETJMP_H_INCLUDED
+#endif
+
+inline int __sigsetjmp(sigjmp_buf env, int savesigs)
+{
+  (void)env;
+  (void)savesigs;
+  // returns via siglongjmp require instrumentation; only such returns would
+  // return a non-zero value
+  return 0;
 }
+
+#endif