1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
extern void __VERIFIER_assume(int);
void __VERIFIER_assert(int cond) {
if (!(cond)) {
ERROR: __VERIFIER_error();
}
return;
}
extern char __VERIFIER_nondet_char();
main()
{
char string_A[5], string_B[5];
int i, j, nc_A, nc_B, found=0;
for(i=0; i<5; i++)
string_A[i]=__VERIFIER_nondet_char();
__VERIFIER_assume(string_A[5 -1]=='\0');
for(i=0; i<5; i++)
string_B[i]=__VERIFIER_nondet_char();
__VERIFIER_assume(string_B[5 -1]=='\0');
nc_A = 0;
while(string_A[nc_A]!='\0')
nc_A++;
nc_B = 0;
while(string_B[nc_B]!='\0')
nc_B++;
__VERIFIER_assume(nc_B >= nc_A);
i=j=0;
while((i<nc_A) && (j<nc_B))
{
if(string_A[i] == string_B[j])
{
i++;
j++;
}
else
{
i = i-j+1;
j = 0;
}
}
found = (j>nc_B-1)<<i;
__VERIFIER_assert(found == 0 || found == 1);
}
|
