cbmc and setjmp

cbmc-output.txt

CBMC version 5.4 64-bit x86_64 macos
Parsing jmptest.c
Converting
Type-checking jmptest
Generating GOTO Program
Adding CPROVER library (x86_64)
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 72 steps
simple slicing removed 6 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
956 variables, 1098 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.003s
Building error trace

Counterexample:

State 19  thread 0
----------------------------------------------------
  argv'[4098]=irep("(\"nil\")")[4098] (?)

State 22 file jmptest.c line 21 thread 0
----------------------------------------------------
  argc=4098 (00000000000000000001000000000010)

State 23 file jmptest.c line 21 thread 0
----------------------------------------------------
  argv=argv' (0000001000000000000000000000000000000000000000000000000000000000)

State 24 file jmptest.c line 23 function main thread 0
----------------------------------------------------
  x=0 (00000000000000000000000000000000)

State 25 file jmptest.c line 23 function main thread 0
----------------------------------------------------
  x=1 (00000000000000000000000000000001)

State 28 file jmptest.c line 28 function main thread 0
----------------------------------------------------
  env=((int *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

State 29 file jmptest.c line 28 function main thread 0
----------------------------------------------------
  env=label (0000001100000000000000000000000000000000000000000000000000000000)

State 30 file <builtin-library-setjmp> line 10 function setjmp thread 0
----------------------------------------------------
  retval=1 (00000000000000000000000000000001)
Caught!


Violated property:
  file jmptest.c line 33 function main
  Exceptional case
  x == 42

VERIFICATION FAILED

setjmp.c

// cbmc jmptest.c -DCBMC

#include <setjmp.h>
#include <stdio.h>
#include <stdlib.h>

jmp_buf label;

void f(int x) {
  if (x == 42) {
    // throw exception
    longjmp(label, 1);
  }
  printf("f(%d)\n", x);
}

#ifdef CBMC
int nondet_int();
#endif

int main(int argc, char **argv) {
#ifdef CBMC
  int x = nondet_int();
#else
  if (argc != 2) return 1;
  int x = atoi(argv[1]);
#endif
  if (0 == setjmp(label)) {
    f(x);
  } else {
    printf("Caught!\n");
#ifdef CBMC
    __CPROVER_assert(x == 42, "Exceptional case");
#endif
  }
  return 0;
}

setjmp and longjmp are modelled by cbmc-trunk/src/ansi-c/library/setjmp.c; these are defined:

inline int setjmp(jmp_buf env)
{
  // store PC
  int retval;
  (void)env;
  return retval;
}

inline void longjmp(jmp_buf env, int val)
{
  // does not return
  (void)env;
  (void)val;
  __CPROVER_assume(0);
}