-
Notifications
You must be signed in to change notification settings - Fork 0
/
max.c
62 lines (54 loc) · 1.17 KB
/
max.c
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
60
61
62
#include <stdio.h>
#include "klee/klee.h"
int buggyQ(int x,int y, int z){
if(x > y){
if(y > z) return x;
else if(x > z) return x;
else return z;
}else{
if(x > z) return y;
else if(y > z) return y;
else
return y; // error location
// return z;
}
}
int correctQ(int x,int y, int z){
if(x > y){
if(y > z) return x;
else if(x > z) return x;
else return z;
}else{
if(x > z) return y;
else if(y > z) return y;
else
return z;
}
}
int mainQ(int x , int y , int z )
{
int rb = buggyQ(x, y, z);
int rc = correctQ(x, y, z);
if (rc==rb) {
printf("PASS with input: x %d, y %d, z%d\n", x, y, z);
return 0;
}
else{
printf("FAIL with input: x %d, y %d, z %d\n", x, y, z);
return 1;
}
}
int main() {
int uk_0, uk_1, uk_2;
klee_make_symbolic(& uk_0, sizeof(uk_0), "uk_0");
klee_assume(-100 <= uk_0);
klee_assume(uk_0 <= 100);
klee_make_symbolic(& uk_1, sizeof(uk_1), "uk_1");
klee_assume(-100 <= uk_1);
klee_assume(uk_1 <= 100);
klee_make_symbolic(& uk_2, sizeof(uk_2), "uk_2");
klee_assume(-100 <= uk_2);
klee_assume(uk_2 <= 100);
int rv = mainQ(uk_0, uk_1, uk_2);
return 0;
}