This is an example of leaping counter-example produced by Loopfrog for the test case apache-cve-2006-3747-4.
It consists of: If you happen to examine it carefully, don't forget that: Switch to fixedbug-version of the same test case.
apache-cve-2006-3747-4/simp2_bad.c

 1 #include "apache.h"
  2
 3 void escape_absolute_uri (char *uri, int scheme)
 4 {
 5   int cp;
 6   char *token[TOKEN_SZ];
 7   int c;
 8
 9   if (scheme == 0
10       || strlen(uri) < scheme) {
11     return;
12   }
13
14   cp = scheme;
15   c = 0;
16
17   token[0] = uri;
18
19   while (uri[cp] != EOS
20          && c < TOKEN_SZ) {
21     if (uri[cp] == '?') {
22       ++c;
23       /* BAD */
24 __TESTCLAIM_1:
25       token[c] = uri + cp + 1;
26       uri[cp] = EOS;
27     }
28     ++cp;
29   }
30
31   return;
32 }
33
34 int main ()
35 {
36   char uri [URI_SZ];
37   int scheme;
38
39   uri [URI_SZ-1] = EOS;
40   scheme = LDAP_SZ + 2;
41
42   escape_absolute_uri (uri, scheme);
43
44   return 0;
45 }
apache-cve-2006-3747-4-fixed/simp2_ok.c

 1 #include "apache.h"
 2
 3 void escape_absolute_uri (char *uri, int scheme)
 4 {
 5   int cp;
 6   char *token[TOKEN_SZ];
 7   int c;
 8
 9   if (scheme == 0
10       || strlen(uri) < scheme) {
11     return;
12   }
13
14   cp = scheme;
15   c = 0;
16
17   token[0] = uri;
18
19   while (uri[cp] != EOS
20          && c < TOKEN_SZ - 1) {
21     if (uri[cp] == '?') {
22       ++c;
23       /* OK */
24 __TESTCLAIM_1:
25       token[c] = uri + cp + 1;
26       uri[cp] = EOS;
27     }
28     ++cp;
29   }
30
31   return;
32 }
33
34 int main ()
35 {
36   char uri [URI_SZ];
37   int scheme;
38
39   uri [URI_SZ-1] = EOS;
40   scheme = LDAP_SZ + 2;
41
42   escape_absolute_uri (uri, scheme);
43
44   return 0;
45 } 
GOTO-PROGRAM:
[... some initialization is stripped away ... ]

        // file simp2_bad.c line 35 function main
          uri#str = { .is_zero=FALSE, .length=(unsigned int)11, .size=(unsigned int)11 };
        // no location
        SKIP
        // no location
        SKIP
        // file simp2_bad.c line 38 function main
          uri[4 + 1 + 1 + 2 + 1 + 2 - 1] = 0;
        // file simp2_bad.c line 38 function main
          uri#str.is_zero = TRUE;
        // file simp2_bad.c line 38 function main
          uri#str.length = (unsigned int)(4 + 1 + 1 + 2 + 1 + 2 - 1) < uri#str.length ? (unsigned int)(4 + 1 + 1 + 2 + 1 + 2 - 1) : uri#str.length;
        // file simp2_bad.c line 39 function main
          scheme = 4 + 2;
        // file simp2_bad.c line 41 function main
          c::simp2_bad::escape_absolute_uri::uri#str = &c::simp2_bad::main::1::uri#str;
        // no location
        SKIP
        // no location
          c::simp2_bad::escape_absolute_uri::uri = &c::simp2_bad::main::1::uri[0];
        // no location
          c::simp2_bad::escape_absolute_uri::scheme = c::simp2_bad::main::1::scheme;
        // no location
        SKIP
        // no location
          tmp$2 = scheme == 0;
        // no location
        IF scheme == 0 THEN GOTO 1
        // file simp2_bad.c line 10 function escape_absolute_uri
        LOCATION
        // file ../stubs/stubs.c line 242 function strlen
          s = uri;
        // file ../stubs/stubs.c line 242 function strlen
          s#str = uri#str;
        // file ../stubs/stubs.c line 243 function strlen
          i = 0;
        // no location
        SKIP
        // no location
        // Labels: VARIANT
          i = NONDET(int);
        // no location
        SKIP
        // file ../stubs/stubs.c line 246 function strlen
          return_value_strlen$3 = (unsigned int)i;
        // no location
        LOCATION
        // file simp2_bad.c line 9 function escape_absolute_uri
     1: IF !(tmp$2 || return_value_strlen$3 < (unsigned int)scheme) THEN GOTO 2
        // no location
        // Labels: DISABLED_GOTO
        ASSUME FALSE
        // file simp2_bad.c line 14 function escape_absolute_uri
     2:   cp = scheme;
        // file simp2_bad.c line 15 function escape_absolute_uri
          c = 0;
        // no location
        SKIP
        // file simp2_bad.c line 17 function escape_absolute_uri
          token[0] = uri;
        // file simp2_bad.c line 17 function escape_absolute_uri
          NULL-object = uri#str;
        // no location
        SKIP
        // no location
        // Labels: PRECONDITION_CHECK
          precondition_check$0 = (&uri#str)->length - POINTER_OFFSET(&uri[0]) < (&uri#str)->size - POINTER_OFFSET(&uri[0]);
        // no location
        // Labels: PRECONDITION_CHECK
          precondition_check$1 = (&uri#str)->is_zero;
        // no location
        // Labels: VARIANT
          token = NONDET(signed char * [3]);
        // no location
        // Labels: VARIANT
          uri = NONDET(signed char [11]);
        // no location
        // Labels: VARIANT
          c = NONDET(int);
        // no location
        // Labels: VARIANT
          cp = NONDET(int);
        // no location
        IF !precondition_check$0 THEN GOTO 3
        // no location
        // Labels: INVARIANT
        ASSUME (&uri#str)->length - POINTER_OFFSET(&uri[0]) < (&uri#str)->size - POINTER_OFFSET(&uri[0])
        // no location
     3: SKIP
        // no location
        IF !precondition_check$1 THEN GOTO 4
        // no location
        // Labels: INVARIANT
        ASSUME (&uri#str)->is_zero
        // no location
     4: SKIP
        // no location
        SKIP
        // no location
        SKIP
        // no location
        SKIP
        // file simp2_bad.c line 19 function escape_absolute_uri
        // Labels: DISABLED_GOTO
        ASSUME (int)(c::simp2_bad::main::1::uri[POINTER_OFFSET(c::simp2_bad::escape_absolute_uri::uri + cp)]) != 0 && c < 2 + 1
        // no location
        SKIP
        // no location
        SKIP
        // file simp2_bad.c line 20 function escape_absolute_uri
        // Labels: DISABLED_GOTO
        ASSUME c::simp2_bad::main::1::uri[POINTER_OFFSET(c::simp2_bad::escape_absolute_uri::uri + cp)] == 63
        // file simp2_bad.c line 21 function escape_absolute_uri
          c = c + 1;
        // no location
        SKIP
        // file simp2_bad.c line 24 function escape_absolute_uri
        ASSERT c < 3 // array `token' upper bound
SYMEX TIME: 0.02
SLICER TIME: 0

EQUATION:
Thread 0 file /usr/include/stdio.h line 142
ASSIGNMENT (STATE)
stdin#1 == NULL
Guard: TRUE
--------------
Thread 0 file /usr/include/stdio.h line 143
ASSIGNMENT (STATE)
stdout#1 == NULL
Guard: TRUE
--------------
Thread 0 file /usr/include/stdio.h line 144
ASSIGNMENT (STATE)
stderr#1 == NULL
Guard: TRUE
--------------
Thread 0 file /usr/include/bits/sys_errlist.h line 27
ASSIGNMENT (STATE)
sys_nerr#1 == 0
Guard: TRUE
--------------
Thread 0 file /usr/include/unistd.h line 474
ASSIGNMENT (STATE)
__environ#1 == NULL
Guard: TRUE
--------------
Thread 0 file  line 12
ASSIGNMENT (STATE)
__CPROVER_alloc#1 == ARRAY_OF(FALSE)
Guard: TRUE
--------------
Thread 0 file  line 13
ASSIGNMENT (STATE)
__CPROVER_alloc_size#1 == ARRAY_OF(0)
Guard: TRUE
--------------
Thread 0 file /usr/include/getopt.h line 59
ASSIGNMENT (STATE)
optarg#1 == NULL
Guard: TRUE
--------------
Thread 0 file /usr/include/getopt.h line 59
ASSIGNMENT (STATE)
optarg#str#1 == NULL
Guard: TRUE
--------------
Thread 0 file /usr/include/getopt.h line 73
ASSIGNMENT (STATE)
optind#1 == 0
Guard: TRUE
--------------
Thread 0 file /usr/include/getopt.h line 78
ASSIGNMENT (STATE)
opterr#1 == 0
Guard: TRUE
--------------
Thread 0 file /usr/include/getopt.h line 82
ASSIGNMENT (STATE)
optopt#1 == 0
Guard: TRUE
--------------
Thread 0
LOCATION
Guard: TRUE
--------------
Thread 0 file simp2_bad.c line 35 function main
ASSIGNMENT (STATE)
uri#str#1 == { .is_zero=FALSE, .length=11, .size=11 }
Guard: TRUE
--------------
Thread 0 file simp2_bad.c line 38 function main
ASSIGNMENT (STATE)
uri#1 == (uri#0 WITH [10:=0])
Guard: TRUE
--------------
Thread 0 file simp2_bad.c line 38 function main
ASSIGNMENT (STATE)
uri#str#2 == (uri#str#1 WITH [is_zero:=TRUE])
Guard: TRUE
--------------
Thread 0 file simp2_bad.c line 38 function main
ASSIGNMENT (STATE)
uri#str#3 == (uri#str#2 WITH [length:=uri#str#2.length > 10 ? 10 : uri#str#2.length])
Guard: TRUE
--------------
Thread 0 file simp2_bad.c line 39 function main
ASSIGNMENT (STATE)
scheme#1 == 6
Guard: TRUE
--------------
Thread 0 file simp2_bad.c line 41 function main
ASSIGNMENT (STATE)
uri#str#1 == &uri#str
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
uri#1 == &uri[0]
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
scheme#1 == 6
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
tmp$2#1 == FALSE
Guard: TRUE
--------------
Thread 0 file simp2_bad.c line 10 function escape_absolute_uri
LOCATION
Guard: TRUE
--------------
Thread 0 file ../stubs/stubs.c line 242 function strlen
ASSIGNMENT (STATE)
s#1 == &uri[0]
Guard: TRUE
--------------
Thread 0 file ../stubs/stubs.c line 242 function strlen
ASSIGNMENT (STATE)
s#str#1 == &uri#str
Guard: TRUE
--------------
Thread 0 file ../stubs/stubs.c line 243 function strlen
ASSIGNMENT (STATE)
i#1 == 0
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
i#2 == nondet_symbol(symex::0)
Guard: TRUE
--------------
Thread 0 file ../stubs/stubs.c line 246 function strlen
ASSIGNMENT (STATE)
return_value_strlen$3#1 == (unsigned int)i#2
Guard: TRUE
--------------
Thread 0
LOCATION
Guard: TRUE
--------------
Thread 0 file simp2_bad.c line 9 function escape_absolute_uri
LOCATION
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (HIDDEN)
\guard#1 == return_value_strlen$3#1 < 6
Guard: TRUE
--------------
Thread 0
ASSUME
\guard#1 => FALSE
Guard: \guard#1
--------------
Thread 0 file simp2_bad.c line 14 function escape_absolute_uri
ASSIGNMENT (STATE)
cp#1 == 6
Guard: TRUE
--------------
Thread 0 file simp2_bad.c line 15 function escape_absolute_uri
ASSIGNMENT (STATE)
c#1 == 0
Guard: TRUE
--------------
Thread 0 file simp2_bad.c line 17 function escape_absolute_uri
ASSIGNMENT (STATE)
token#1 == (token#0 WITH [0:=&uri[0]])
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
precondition_check$0#1 == !(uri#str#3.length >= uri#str#3.size)
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
precondition_check$1#1 == uri#str#3.is_zero
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
token#2 == nondet_symbol(symex::1)
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
uri#2 == nondet_symbol(symex::2)
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
c#2 == nondet_symbol(symex::3)
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
cp#2 == nondet_symbol(symex::4)
Guard: TRUE
--------------
Thread 0
LOCATION
Guard: TRUE
--------------
Thread 0
ASSUME
precondition_check$0#1 => uri#str#3.length - POINTER_OFFSET(&uri[0]) < uri#str#3.size - POINTER_OFFSET(&uri[0])
Guard: precondition_check$0#1
--------------
Thread 0
LOCATION
Guard: TRUE
--------------
Thread 0
ASSUME
precondition_check$1#1 => uri#str#3.is_zero
Guard: precondition_check$1#1
--------------
Thread 0 file simp2_bad.c line 19 function escape_absolute_uri
ASSUME
(int)(uri#2[POINTER_OFFSET(&uri[0] + cp#2)]) != 0 && c#2 < 2 + 1
Guard: TRUE
--------------
Thread 0 file simp2_bad.c line 20 function escape_absolute_uri
ASSUME
uri#2[POINTER_OFFSET(&uri[0] + cp#2)] == 63
Guard: TRUE
--------------
Thread 0 file simp2_bad.c line 21 function escape_absolute_uri
ASSIGNMENT (STATE)
c#3 == 1 + c#2
Guard: TRUE
--------------
Thread 0 file simp2_bad.c line 24 function escape_absolute_uri
ASSERT
c#3 < 3
array `token' upper bound
Guard: TRUE
--------------

RESULT:
Solving with MiniSAT
SOLVER TIME: 0.001
SAT - doesn't hold

State 1 file /usr/include/stdio.h line 142 thread 0
----------------------------------------------------
  stdin=(assignment removed)

State 2 file /usr/include/stdio.h line 143 thread 0
----------------------------------------------------
  stdout=(assignment removed)

State 3 file /usr/include/stdio.h line 144 thread 0
----------------------------------------------------
  stderr=(assignment removed)

State 4 file /usr/include/bits/sys_errlist.h line 27 thread 0
----------------------------------------------------
  sys_nerr=(assignment removed)

State 5 file /usr/include/unistd.h line 474 thread 0
----------------------------------------------------
  __environ=(assignment removed)

State 6 file  line 12 thread 0
----------------------------------------------------
  __CPROVER_alloc=(assignment removed)

State 7 file  line 13 thread 0
----------------------------------------------------
  __CPROVER_alloc_size=(assignment removed)

State 8 file /usr/include/getopt.h line 59 thread 0
----------------------------------------------------
  optarg=(assignment removed)

State 9 file /usr/include/getopt.h line 59 thread 0
----------------------------------------------------
  optarg#str=(assignment removed)

State 10 file /usr/include/getopt.h line 73 thread 0
----------------------------------------------------
  optind=(assignment removed)

State 11 file /usr/include/getopt.h line 78 thread 0
----------------------------------------------------
  opterr=(assignment removed)

State 12 file /usr/include/getopt.h line 82 thread 0
----------------------------------------------------
  optopt=(assignment removed)

State 14 file simp2_bad.c line 35 function main thread 0
----------------------------------------------------
  simp2_bad::main::1::uri#str={ .is_zero=FALSE, .length=11, .size=11 }

State 15 file simp2_bad.c line 38 function main thread 0
----------------------------------------------------
  simp2_bad::main::1::uri=(assignment removed)

State 16 file simp2_bad.c line 38 function main thread 0
----------------------------------------------------
  simp2_bad::main::1::uri#str={ .is_zero=TRUE, .length=11, .size=11 }

State 17 file simp2_bad.c line 38 function main thread 0
----------------------------------------------------
  simp2_bad::main::1::uri#str={ .is_zero=TRUE, .length=10, .size=11 }

State 18 file simp2_bad.c line 39 function main thread 0
----------------------------------------------------
  simp2_bad::main::1::scheme=(assignment removed)

State 19 file simp2_bad.c line 41 function main thread 0
----------------------------------------------------
  simp2_bad::escape_absolute_uri::uri#str=(assignment removed)

State 20  thread 0
----------------------------------------------------
  simp2_bad::escape_absolute_uri::uri=(assignment removed)

State 21  thread 0
----------------------------------------------------
  simp2_bad::escape_absolute_uri::scheme=(assignment removed)

State 22  thread 0
----------------------------------------------------
  c::escape_absolute_uri::$tmp::tmp$2=(assignment removed)

State 24 file ../stubs/stubs.c line 242 function strlen thread 0
----------------------------------------------------
  stubs::strlen::s=(assignment removed)

State 25 file ../stubs/stubs.c line 242 function strlen thread 0
----------------------------------------------------
  stubs::strlen::s#str=(assignment removed)

State 26 file ../stubs/stubs.c line 243 function strlen thread 0
----------------------------------------------------
  stubs::strlen::1::i=(assignment removed)

State 27  thread 0
----------------------------------------------------
  stubs::strlen::1::i=-2147483648 (10000000000000000000000000000000)

State 28 file ../stubs/stubs.c line 246 function strlen thread 0
----------------------------------------------------
  c::escape_absolute_uri::$tmp::return_value_strlen$3=2147483648 (10000000000000000000000000000000)

State 31 file simp2_bad.c line 14 function escape_absolute_uri thread 0
----------------------------------------------------
  simp2_bad::escape_absolute_uri::1::cp=(assignment removed)

State 32 file simp2_bad.c line 15 function escape_absolute_uri thread 0
----------------------------------------------------
  simp2_bad::escape_absolute_uri::1::c=(assignment removed)

State 33 file simp2_bad.c line 17 function escape_absolute_uri thread 0
----------------------------------------------------
  simp2_bad::escape_absolute_uri::1::token=(assignment removed)

State 34  thread 0
----------------------------------------------------
  precondition_check$0=TRUE

State 35  thread 0
----------------------------------------------------
  precondition_check$1=TRUE

State 36  thread 0
----------------------------------------------------
  simp2_bad::escape_absolute_uri::1::token=(assignment removed)

State 37  thread 0
----------------------------------------------------
  simp2_bad::main::1::uri={ 62, 62, 62, 62, 62, 62, 62, 62, 62, 62, 62 }

State 38  thread 0
----------------------------------------------------
  simp2_bad::escape_absolute_uri::1::c=2 (00000000000000000000000000000010)

State 39  thread 0
----------------------------------------------------
  simp2_bad::escape_absolute_uri::1::cp=12 (00000000000000000000000000001100)

State 46 file simp2_bad.c line 21 function escape_absolute_uri thread 0
----------------------------------------------------
  simp2_bad::escape_absolute_uri::1::c=3 (00000000000000000000000000000011)

Violated property:
  file simp2_bad.c line 24 function escape_absolute_uri
  array `token' upper bound
  c < 3



GOTO-PROGRAM:
[... some initialization is stripped away ... ]

        // file simp2_ok.c line 35 function main
          uri#str = { .is_zero=FALSE, .length=(unsigned int)11, .size=(unsigned int)11 };
        // no location
        SKIP
        // no location
        SKIP
        // file simp2_ok.c line 38 function main
          uri[4 + 1 + 1 + 2 + 1 + 2 - 1] = 0;
        // file simp2_ok.c line 38 function main
          uri#str.is_zero = TRUE;
        // file simp2_ok.c line 38 function main
          uri#str.length = (unsigned int)(4 + 1 + 1 + 2 + 1 + 2 - 1) < uri#str.length ? (unsigned int)(4 + 1 + 1 + 2 + 1 + 2 - 1) : uri#str.length;
        // file simp2_ok.c line 39 function main
          scheme = 4 + 2;
        // file simp2_ok.c line 41 function main
          c::simp2_ok::escape_absolute_uri::uri#str = &c::simp2_ok::main::1::uri#str;
        // no location
        SKIP
        // no location
          c::simp2_ok::escape_absolute_uri::uri = &c::simp2_ok::main::1::uri[0];
        // no location
          c::simp2_ok::escape_absolute_uri::scheme = c::simp2_ok::main::1::scheme;
        // no location
        SKIP
        // no location
          tmp$2 = scheme == 0;
        // no location
        IF scheme == 0 THEN GOTO 1
        // file simp2_ok.c line 10 function escape_absolute_uri
        LOCATION
        // file ../stubs/stubs.c line 242 function strlen
          s = uri;
        // file ../stubs/stubs.c line 242 function strlen
          s#str = uri#str;
        // file ../stubs/stubs.c line 243 function strlen
          i = 0;
        // no location
        SKIP
        // no location
        // Labels: VARIANT
          i = NONDET(int);
        // no location
        SKIP
        // file ../stubs/stubs.c line 246 function strlen
          return_value_strlen$3 = (unsigned int)i;
        // no location
        LOCATION
        // file simp2_ok.c line 9 function escape_absolute_uri
     1: IF !(tmp$2 || return_value_strlen$3 < (unsigned int)scheme) THEN GOTO 2
        // no location
        // Labels: DISABLED_GOTO
        ASSUME FALSE
        // file simp2_ok.c line 14 function escape_absolute_uri
     2:   cp = scheme;
        // file simp2_ok.c line 15 function escape_absolute_uri
          c = 0;
        // no location
        SKIP
        // file simp2_ok.c line 17 function escape_absolute_uri
          token[0] = uri;
        // file simp2_ok.c line 17 function escape_absolute_uri
          NULL-object = uri#str;
        // no location
        SKIP
        // no location
        // Labels: PRECONDITION_CHECK
          precondition_check$0 = (&uri#str)->length - POINTER_OFFSET(&uri[0]) < (&uri#str)->size - POINTER_OFFSET(&uri[0]);
        // no location
        // Labels: PRECONDITION_CHECK
          precondition_check$1 = (&uri#str)->is_zero;
        // no location
        // Labels: VARIANT
          token = NONDET(signed char * [3]);
        // no location
        // Labels: VARIANT
          uri = NONDET(signed char [11]);
        // no location
        // Labels: VARIANT
          c = NONDET(int);
        // no location
        // Labels: VARIANT
          cp = NONDET(int);
        // no location
        IF !precondition_check$0 THEN GOTO 3
        // no location
        // Labels: INVARIANT
        ASSUME (&uri#str)->length - POINTER_OFFSET(&uri[0]) < (&uri#str)->size - POINTER_OFFSET(&uri[0])
        // no location
     3: SKIP
        // no location
        IF !precondition_check$1 THEN GOTO 4
        // no location
        // Labels: INVARIANT
        ASSUME (&uri#str)->is_zero
        // no location
     4: SKIP
        // no location
        SKIP
        // no location
        SKIP
        // no location
        SKIP
        // file simp2_ok.c line 19 function escape_absolute_uri
        // Labels: DISABLED_GOTO
        ASSUME (int)(c::simp2_ok::main::1::uri[POINTER_OFFSET(c::simp2_ok::escape_absolute_uri::uri + cp)]) != 0 && c < 2 + 1 - 1
        // no location
        SKIP
        // no location
        SKIP
        // file simp2_ok.c line 20 function escape_absolute_uri
        // Labels: DISABLED_GOTO
        ASSUME c::simp2_ok::main::1::uri[POINTER_OFFSET(c::simp2_ok::escape_absolute_uri::uri + cp)] == 63
        // file simp2_ok.c line 21 function escape_absolute_uri
          c = c + 1;
        // no location
        SKIP
        // file simp2_ok.c line 24 function escape_absolute_uri
        ASSERT c < 3 // array `token' upper bound
SYMEX TIME: 0.024
SLICER TIME: 0

EQUATION:
Thread 0 file /usr/include/stdio.h line 142
ASSIGNMENT (STATE)
stdin#1 == NULL
Guard: TRUE
--------------
Thread 0 file /usr/include/stdio.h line 143
ASSIGNMENT (STATE)
stdout#1 == NULL
Guard: TRUE
--------------
Thread 0 file /usr/include/stdio.h line 144
ASSIGNMENT (STATE)
stderr#1 == NULL
Guard: TRUE
--------------
Thread 0 file /usr/include/bits/sys_errlist.h line 27
ASSIGNMENT (STATE)
sys_nerr#1 == 0
Guard: TRUE
--------------
Thread 0 file /usr/include/unistd.h line 474
ASSIGNMENT (STATE)
__environ#1 == NULL
Guard: TRUE
--------------
Thread 0 file  line 12
ASSIGNMENT (STATE)
__CPROVER_alloc#1 == ARRAY_OF(FALSE)
Guard: TRUE
--------------
Thread 0 file  line 13
ASSIGNMENT (STATE)
__CPROVER_alloc_size#1 == ARRAY_OF(0)
Guard: TRUE
--------------
Thread 0 file /usr/include/getopt.h line 59
ASSIGNMENT (STATE)
optarg#1 == NULL
Guard: TRUE
--------------
Thread 0 file /usr/include/getopt.h line 59
ASSIGNMENT (STATE)
optarg#str#1 == NULL
Guard: TRUE
--------------
Thread 0 file /usr/include/getopt.h line 73
ASSIGNMENT (STATE)
optind#1 == 0
Guard: TRUE
--------------
Thread 0 file /usr/include/getopt.h line 78
ASSIGNMENT (STATE)
opterr#1 == 0
Guard: TRUE
--------------
Thread 0 file /usr/include/getopt.h line 82
ASSIGNMENT (STATE)
optopt#1 == 0
Guard: TRUE
--------------
Thread 0
LOCATION
Guard: TRUE
--------------
Thread 0 file simp2_ok.c line 35 function main
ASSIGNMENT (STATE)
uri#str#1 == { .is_zero=FALSE, .length=11, .size=11 }
Guard: TRUE
--------------
Thread 0 file simp2_ok.c line 38 function main
ASSIGNMENT (STATE)
uri#1 == (uri#0 WITH [10:=0])
Guard: TRUE
--------------
Thread 0 file simp2_ok.c line 38 function main
ASSIGNMENT (STATE)
uri#str#2 == (uri#str#1 WITH [is_zero:=TRUE])
Guard: TRUE
--------------
Thread 0 file simp2_ok.c line 38 function main
ASSIGNMENT (STATE)
uri#str#3 == (uri#str#2 WITH [length:=uri#str#2.length > 10 ? 10 : uri#str#2.length])
Guard: TRUE
--------------
Thread 0 file simp2_ok.c line 39 function main
ASSIGNMENT (STATE)
scheme#1 == 6
Guard: TRUE
--------------
Thread 0 file simp2_ok.c line 41 function main
ASSIGNMENT (STATE)
uri#str#1 == &uri#str
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
uri#1 == &uri[0]
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
scheme#1 == 6
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
tmp$2#1 == FALSE
Guard: TRUE
--------------
Thread 0 file simp2_ok.c line 10 function escape_absolute_uri
LOCATION
Guard: TRUE
--------------
Thread 0 file ../stubs/stubs.c line 242 function strlen
ASSIGNMENT (STATE)
s#1 == &uri[0]
Guard: TRUE
--------------
Thread 0 file ../stubs/stubs.c line 242 function strlen
ASSIGNMENT (STATE)
s#str#1 == &uri#str
Guard: TRUE
--------------
Thread 0 file ../stubs/stubs.c line 243 function strlen
ASSIGNMENT (STATE)
i#1 == 0
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
i#2 == nondet_symbol(symex::0)
Guard: TRUE
--------------
Thread 0 file ../stubs/stubs.c line 246 function strlen
ASSIGNMENT (STATE)
return_value_strlen$3#1 == (unsigned int)i#2
Guard: TRUE
--------------
Thread 0
LOCATION
Guard: TRUE
--------------
Thread 0 file simp2_ok.c line 9 function escape_absolute_uri
LOCATION
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (HIDDEN)
\guard#1 == return_value_strlen$3#1 < 6
Guard: TRUE
--------------
Thread 0
ASSUME
\guard#1 => FALSE
Guard: \guard#1
--------------
Thread 0 file simp2_ok.c line 14 function escape_absolute_uri
ASSIGNMENT (STATE)
cp#1 == 6
Guard: TRUE
--------------
Thread 0 file simp2_ok.c line 15 function escape_absolute_uri
ASSIGNMENT (STATE)
c#1 == 0
Guard: TRUE
--------------
Thread 0 file simp2_ok.c line 17 function escape_absolute_uri
ASSIGNMENT (STATE)
token#1 == (token#0 WITH [0:=&uri[0]])
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
precondition_check$0#1 == !(uri#str#3.length >= uri#str#3.size)
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
precondition_check$1#1 == uri#str#3.is_zero
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
token#2 == nondet_symbol(symex::1)
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
uri#2 == nondet_symbol(symex::2)
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
c#2 == nondet_symbol(symex::3)
Guard: TRUE
--------------
Thread 0
ASSIGNMENT (STATE)
cp#2 == nondet_symbol(symex::4)
Guard: TRUE
--------------
Thread 0
LOCATION
Guard: TRUE
--------------
Thread 0
ASSUME
precondition_check$0#1 => uri#str#3.length - POINTER_OFFSET(&uri[0]) < uri#str#3.size - POINTER_OFFSET(&uri[0])
Guard: precondition_check$0#1
--------------
Thread 0
LOCATION
Guard: TRUE
--------------
Thread 0
ASSUME
precondition_check$1#1 => uri#str#3.is_zero
Guard: precondition_check$1#1
--------------
Thread 0 file simp2_ok.c line 19 function escape_absolute_uri
ASSUME
(int)(uri#2[POINTER_OFFSET(&uri[0] + cp#2)]) != 0 && c#2 < 2 + 1 - 1
Guard: TRUE
--------------
Thread 0 file simp2_ok.c line 20 function escape_absolute_uri
ASSUME
uri#2[POINTER_OFFSET(&uri[0] + cp#2)] == 63
Guard: TRUE
--------------
Thread 0 file simp2_ok.c line 21 function escape_absolute_uri
ASSIGNMENT (STATE)
c#3 == 1 + c#2
Guard: TRUE
--------------
Thread 0 file simp2_ok.c line 24 function escape_absolute_uri
ASSERT
c#3 < 3
array `token' upper bound
Guard: TRUE
--------------

RESULT:
Solving with MiniSAT
SOLVER TIME: 0.002
UNSAT - it holds!

ASSERTION IS TRUE