Skip to content

Commit 57af54c

Browse files
thk123thk123
authored
Merge pull request #164 from diffblue/feature/last_written_locations
Context aware merge
2 parents bcccaca + 417c476 commit 57af54c

File tree

48 files changed

+1587
-67
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

48 files changed

+1587
-67
lines changed

‎regression/goto-analyzer/sensitivity-last-written-locations-arrays/sensitivity_dependency_arrays.c

+50
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
int main()
2+
{
3+
do_arrays();
4+
}
5+
6+
void do_arrays()
7+
{
8+
int bool_;
9+
int bool_1;
10+
int bool_2;
11+
12+
int x[2];
13+
14+
// Simple variables.
15+
x[0]=10;
16+
x[1]=20;
17+
x[0]=30;
18+
x[1]=40;
19+
x[1]=x[0];
20+
x[0]=x[1];
21+
x[0]=5;
22+
x[0]=x[0]+10;
23+
x[1]=10;
24+
25+
if(bool_)
26+
{
27+
x[0]=20;
28+
}
29+
else
30+
{
31+
x[0]=20;
32+
}
33+
34+
x[0]=0;
35+
36+
if(bool_1)
37+
{
38+
x[0]=3;
39+
if(bool_2)
40+
{
41+
x[0]=5;
42+
}
43+
}
44+
else
45+
{
46+
x[0]=7;
47+
}
48+
x[1]=10;
49+
x[0]=20;
50+
}

‎regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc

+41
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
CORE
2+
sensitivity_dependency_arrays.c
3+
--variable --arrays --pointers --structs
4+
// Enable multi-line checking
5+
activate-multi-line-match
6+
__CPROVER_threads_exited \(\) -> TOP @ \[14\]
7+
__CPROVER_malloc_is_new_array \(\) -> false @ \[6\]
8+
__CPROVER_dead_object \(\) -> TOP @ \[4\]
9+
__CPROVER_deallocated \(\) -> TOP @ \[5\]
10+
__CPROVER_malloc_object \(\) -> TOP @ \[7\]
11+
__CPROVER_memory_leak \(\) -> TOP @ \[9\]
12+
__CPROVER_rounding_mode \(\) -> 00000000000000000000000000000000 @ \[12\]
13+
__CPROVER_pipe_count \(\) -> 00000000000000000000000000000000 @ \[11\]
14+
__CPROVER_malloc_size \(\) -> 0000000000000000000000000000000000000000000000000000000000000000 @ \[8\]
15+
__CPROVER_next_thread_id \(\) -> 0000000000000000000000000000000000000000000000000000000000000000 @ \[10\]
16+
__CPROVER_thread_id \(\) -> 0000000000000000000000000000000000000000000000000000000000000000 @ \[13\]
17+
do_arrays#return_value \(\) -> TOP @ \[49\]
18+
main#return_value \(\) -> TOP @ \[1\]
19+
do_arrays::1::bool_ \(\) -> TOP @ \[16\]
20+
do_arrays::1::bool_1 \(\) -> TOP @ \[17\]
21+
do_arrays::1::bool_2 \(\) -> TOP @ \[18\]
22+
do_arrays::1::x \(\) -> \{\[0\] = 00000000000000000000000000011110 @ \[22\]\n\[1\] = 00000000000000000000000000010100 @ \[21\]\n\} @ \[22\]
23+
do_arrays::1::x \(\) -> \{\[0\] = 00000000000000000000000000011110 @ \[22\]\n\[1\] = 00000000000000000000000000101000 @ \[23\]\n\} @ \[23\]
24+
do_arrays::1::x \(\) -> \{\[0\] = 00000000000000000000000000011110 @ \[22\]\n\[1\] = 00000000000000000000000000011110 @ \[24\]\n\} @ \[24\]
25+
do_arrays::1::x \(\) -> \{\[0\] = 00000000000000000000000000011110 @ \[25\]\n\[1\] = 00000000000000000000000000011110 @ \[24\]\n\} @ \[25\]
26+
do_arrays::1::x \(\) -> \{\[0\] = 00000000000000000000000000000101 @ \[26\]\n\[1\] = 00000000000000000000000000011110 @ \[24\]\n\} @ \[26\]
27+
do_arrays::1::x \(\) -> \{\[0\] = 00000000000000000000000000001111 @ \[27\]\n\[1\] = 00000000000000000000000000011110 @ \[24\]\n\} @ \[27\]
28+
do_arrays::1::x \(\) -> \{\[0\] = 00000000000000000000000000001111 @ \[27\]\n\[1\] = 00000000000000000000000000001010 @ \[28\]\n\} @ \[28\]
29+
do_arrays::1::x \(\) -> \{\[0\] = 00000000000000000000000000001111 @ \[27\]\n\[1\] = 00000000000000000000000000001010 @ \[28\]\n\} @ \[28\]
30+
do_arrays::1::x \(\) -> \{\[0\] = 00000000000000000000000000010100 @ \[30\]\n\[1\] = 00000000000000000000000000001010 @ \[28\]\n\} @ \[30\]
31+
do_arrays::1::x \(\) -> \{\[0\] = 00000000000000000000000000001111 @ \[27\]\n\[1\] = 00000000000000000000000000001010 @ \[28\]\n\} @ \[28\]
32+
do_arrays::1::x \(\) -> \{\[0\] = 00000000000000000000000000010100 @ \[30\, 32\]\n\[1\] = 00000000000000000000000000001010 @ \[28\]\n\} @ \[30\, 32\]
33+
do_arrays::1::x \(\) -> \{\[0\] = 00000000000000000000000000000000 @ \[34\]\n\[1\] = 00000000000000000000000000001010 @ \[28\]\n\} @ \[34\]
34+
do_arrays::1::x \(\) -> \{\[0\] = 00000000000000000000000000000011 @ \[36\]\n\[1\] = 00000000000000000000000000001010 @ \[28\]\n\} @ \[36\]
35+
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[36\, 38\]\n\[1\] = 00000000000000000000000000001010 @ \[28\]\n\} @ \[36\, 38\]
36+
do_arrays::1::x \(\) -> \{\[0\] = 00000000000000000000000000000000 @ \[34\]\n\[1\] = 00000000000000000000000000001010 @ \[28\]\n\} @ \[34\]
37+
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[36\, 38\, 41\]\n\[1\] = 00000000000000000000000000001010 @ \[28\]\n\} @ \[36\, 38\, 41\]
38+
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[36\, 38\, 41\]\n\[1\] = 00000000000000000000000000001010 @ \[28\]\n\} @ \[36\, 38\, 41\]
39+
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[36\, 38\, 41\]\n\[1\] = 00000000000000000000000000001010 @ \[43\]\n\} @ \[43\]
40+
do_arrays::1::x \(\) -> \{\[0\] = 00000000000000000000000000010100 @ \[44\]\n\[1\] = 00000000000000000000000000001010 @ \[43\]\n\} @ \[44\]
41+
--

‎regression/goto-analyzer/sensitivity-last-written-locations-pointers/sensitivity_dependency_pointers.c

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
int main()
2+
{
3+
do_pointers();
4+
}
5+
6+
void do_pointers()
7+
{
8+
int bool_;
9+
int bool_1;
10+
int bool_2;
11+
12+
int x=10;
13+
int *x_p;
14+
15+
int y=20;
16+
int *y_p;
17+
18+
x_p=&x;
19+
20+
*x_p=30;
21+
x=40;
22+
23+
*x_p=*y_p;
24+
x=50;
25+
y_p=&x;
26+
27+
*x_p=60;
28+
29+
int j=*y_p;
30+
}

‎regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc

+37
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
CORE
2+
sensitivity_dependency_pointers.c
3+
--variable --arrays --pointers --structs
4+
// Enable multi-line checking
5+
activate-multi-line-match
6+
__CPROVER_threads_exited \(\) -> TOP @ \[14\]
7+
__CPROVER_malloc_is_new_array \(\) -> false @ \[6\]
8+
__CPROVER_dead_object \(\) -> TOP @ \[4\]
9+
__CPROVER_deallocated \(\) -> TOP @ \[5\]
10+
__CPROVER_malloc_object \(\) -> TOP @ \[7\]
11+
__CPROVER_memory_leak \(\) -> TOP @ \[9\]
12+
__CPROVER_rounding_mode \(\) -> 00000000000000000000000000000000 @ \[12\]
13+
__CPROVER_pipe_count \(\) -> 00000000000000000000000000000000 @ \[11\]
14+
__CPROVER_malloc_size \(\) -> 0000000000000000000000000000000000000000000000000000000000000000 @ \[8\]
15+
__CPROVER_next_thread_id \(\) -> 0000000000000000000000000000000000000000000000000000000000000000 @ \[10\]
16+
__CPROVER_thread_id \(\) -> 0000000000000000000000000000000000000000000000000000000000000000 @ \[13\]
17+
do_pointers#return_value \(\) -> TOP @ \[42\]
18+
main#return_value \(\) -> TOP @ \[1\]
19+
do_pointers::1::bool_ \(\) -> TOP @ \[16\]
20+
do_pointers::1::bool_1 \(\) -> TOP @ \[17\]
21+
do_pointers::1::bool_2 \(\) -> TOP @ \[18\]
22+
do_pointers::1::x \(\) -> TOP @ \[19\]
23+
do_pointers::1::x \(\) -> 00000000000000000000000000001010 @ \[20\]
24+
do_pointers::1::x_p \(\) -> TOP @ \[21\]
25+
do_pointers::1::y \(\) -> TOP @ \[22\]
26+
do_pointers::1::y \(\) -> 00000000000000000000000000010100 @ \[23\]
27+
do_pointers::1::y_p \(\) -> TOP @ \[24\]
28+
do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[25\]
29+
do_pointers::1::x \(\) -> 00000000000000000000000000011110 @ \[26\]
30+
do_pointers::1::x \(\) -> 00000000000000000000000000101000 @ \[27\]
31+
do_pointers::1::x \(\) -> TOP @ \[28\]
32+
do_pointers::1::x \(\) -> 00000000000000000000000000110010 @ \[29\]
33+
do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[30\]
34+
do_pointers::1::x \(\) -> 00000000000000000000000000111100 @ \[31\]
35+
do_pointers::1::j \(\) -> TOP @ \[32\]
36+
do_pointers::1::j \(\) -> 00000000000000000000000000111100 @ \[33\]
37+
--

‎regression/goto-analyzer/sensitivity-last-written-locations-structs/sensitivity_dependency_structs.c

+59
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
int main()
2+
{
3+
do_structs();
4+
}
5+
6+
struct Ages {
7+
int x;
8+
int y;
9+
};
10+
11+
void do_structs()
12+
{
13+
int bool_;
14+
int bool_1;
15+
int bool_2;
16+
17+
struct Ages st;
18+
19+
// Simple variables.
20+
st.x=10;
21+
st.y=20;
22+
st.x=30;
23+
st.y=40;
24+
st.y=st.x;
25+
st.x=st.y;
26+
st.x=5;
27+
st.x=st.x+10;
28+
st.y=10;
29+
30+
if(bool_)
31+
{
32+
st.x=20;
33+
}
34+
else
35+
{
36+
st.x=20;
37+
}
38+
39+
st.x=0;
40+
41+
if(bool_1)
42+
{
43+
st.x=3;
44+
if(bool_2)
45+
{
46+
st.x=5;
47+
}
48+
}
49+
else
50+
{
51+
st.x=7;
52+
}
53+
st.y=10;
54+
st.x=20;
55+
56+
struct Ages new_age;
57+
58+
new_age=st;
59+
}

‎regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc

+50
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
CORE
2+
sensitivity_dependency_structs.c
3+
--variable --arrays --pointers --structs
4+
// Enable multi-line checking
5+
activate-multi-line-match
6+
__CPROVER_threads_exited \(\) -> TOP @ \[14\]
7+
__CPROVER_malloc_is_new_array \(\) -> false @ \[6\]
8+
__CPROVER_dead_object \(\) -> TOP @ \[4\]
9+
__CPROVER_deallocated \(\) -> TOP @ \[5\]
10+
__CPROVER_malloc_object \(\) -> TOP @ \[7\]
11+
__CPROVER_memory_leak \(\) -> TOP @ \[9\]
12+
__CPROVER_rounding_mode \(\) -> 00000000000000000000000000000000 @ \[12\]
13+
__CPROVER_pipe_count \(\) -> 00000000000000000000000000000000 @ \[11\]
14+
__CPROVER_malloc_size \(\) -> 0000000000000000000000000000000000000000000000000000000000000000 @ \[8\]
15+
__CPROVER_next_thread_id \(\) -> 0000000000000000000000000000000000000000000000000000000000000000 @ \[10\]
16+
__CPROVER_thread_id \(\) -> 0000000000000000000000000000000000000000000000000000000000000000 @ \[13\]
17+
do_structs#return_value \(\) -> TOP @ \[52\]
18+
main#return_value \(\) -> TOP @ \[1\]
19+
do_structs::1::bool_ \(\) -> TOP @ \[16\]
20+
do_structs::1::bool_1 \(\) -> TOP @ \[17\]
21+
do_structs::1::bool_2 \(\) -> TOP @ \[18\]
22+
do_structs::1::st \(\) -> \{\} @ \[19\]
23+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000001010 @ \[20\]\} @ \[20\]
24+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000001010 @ \[20\]\, .y=00000000000000000000000000010100 @ \[21\]\} @ \[21\]
25+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000011110 @ \[22\]\, .y=00000000000000000000000000010100 @ \[21\]\} @ \[22\]
26+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000011110 @ \[22\]\, .y=00000000000000000000000000101000 @ \[23\]\} @ \[23\]
27+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000011110 @ \[22\]\, .y=00000000000000000000000000011110 @ \[24\]\} @ \[24\]
28+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000011110 @ \[25\]\, .y=00000000000000000000000000011110 @ \[24\]\} @ \[25\]
29+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000000101 @ \[26\]\, .y=00000000000000000000000000011110 @ \[24\]\} @ \[26\]
30+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000001111 @ \[27\]\, .y=00000000000000000000000000011110 @ \[24\]\} @ \[27\]
31+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000001111 @ \[27\]\, .y=00000000000000000000000000001010 @ \[28\]\} @ \[28\]
32+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000001111 @ \[27\]\, .y=00000000000000000000000000001010 @ \[28\]\} @ \[28\]
33+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000010100 @ \[30\]\, .y=00000000000000000000000000001010 @ \[28\]\} @ \[30\]
34+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000001111 @ \[27\]\, .y=00000000000000000000000000001010 @ \[28\]\} @ \[28\]
35+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000010100 @ \[30\, 32\]\, .y=00000000000000000000000000001010 @ \[28\]\} @ \[30\, 32\]
36+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000010100 @ \[30\, 32\]\, .y=00000000000000000000000000001010 @ \[28\]\} @ \[30\, 32\]
37+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000000000 @ \[34\]\, .y=00000000000000000000000000001010 @ \[28\]\} @ \[34\]
38+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000000000 @ \[34\]\, .y=00000000000000000000000000001010 @ \[28\]\} @ \[34\]
39+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000000011 @ \[36\]\, .y=00000000000000000000000000001010 @ \[28\]\} @ \[36\]
40+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000000011 @ \[36\]\, .y=00000000000000000000000000001010 @ \[28\]\} @ \[36\]
41+
do_structs::1::st \(\) -> \{.x=TOP @ \[36\, 38\]\, .y=00000000000000000000000000001010 @ \[28\]\} @ \[36\, 38\]
42+
do_structs::1::st \(\) -> \{.x=TOP @ \[36\, 38\]\, .y=00000000000000000000000000001010 @ \[28\]\} @ \[36\, 38\]
43+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000000000 @ \[34\]\, .y=00000000000000000000000000001010 @ \[28\]\} @ \[34\]
44+
do_structs::1::st \(\) -> \{.x=TOP @ \[36\, 38\, 41\]\, .y=00000000000000000000000000001010 @ \[28\]\} @ \[36\, 38\, 41\]
45+
do_structs::1::st \(\) -> \{.x=TOP @ \[36\, 38\, 41\]\, .y=00000000000000000000000000001010 @ \[28\]\} @ \[36\, 38\, 41\]
46+
do_structs::1::st \(\) -> \{.x=TOP @ \[36\, 38\, 41\]\, .y=00000000000000000000000000001010 @ \[43\]\} @ \[43\]
47+
do_structs::1::st \(\) -> \{.x=00000000000000000000000000010100 @ \[44\]\, .y=00000000000000000000000000001010 @ \[43\]\} @ \[44\]
48+
do_structs::1::new_age \(\) -> \{\} @ \[45\]
49+
do_structs::1::new_age \(\) -> \{.x=00000000000000000000000000010100 @ \[46\]\, .y=00000000000000000000000000001010 @ \[46\]\} @ \[46\]
50+
--

‎regression/goto-analyzer/sensitivity-last-written-locations-variables/sensitivity_dependency_variables.c

+63
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
int global_x; // Should assign to 0.
2+
3+
int main()
4+
{
5+
do_variables();
6+
}
7+
8+
void do_variables()
9+
{
10+
int bool_;
11+
int bool_1;
12+
int bool_2;
13+
14+
global_x=5;
15+
16+
// Simple variables.
17+
int x=10;
18+
int y=20;
19+
x=30;
20+
y=40;
21+
y=x;
22+
x=y;
23+
x=5;
24+
x=x+10;
25+
y=10;
26+
27+
if(bool_)
28+
{
29+
x=20;
30+
}
31+
else
32+
{
33+
x=20;
34+
}
35+
36+
x=50;
37+
38+
if(bool_)
39+
{
40+
x=20;
41+
}
42+
else
43+
{
44+
x=30;
45+
}
46+
47+
x=0;
48+
49+
if(bool_1)
50+
{
51+
x=3;
52+
if(bool_2)
53+
{
54+
x=5;
55+
}
56+
}
57+
else
58+
{
59+
x=7;
60+
}
61+
y=10;
62+
x=20;
63+
}

‎regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc

+47
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
CORE
2+
sensitivity_dependency_variables.c
3+
--variable --arrays --pointers --structs
4+
// Enable multi-line checking
5+
activate-multi-line-match
6+
__CPROVER_threads_exited \(\) -> TOP @ \[14\]
7+
__CPROVER_malloc_is_new_array \(\) -> false @ \[6\]
8+
__CPROVER_dead_object \(\) -> TOP @ \[4\]
9+
__CPROVER_deallocated \(\) -> TOP @ \[5\]
10+
__CPROVER_malloc_object \(\) -> TOP @ \[7\]
11+
__CPROVER_memory_leak \(\) -> TOP @ \[9\]
12+
__CPROVER_rounding_mode \(\) -> 00000000000000000000000000000000 @ \[12\]
13+
global_x \(\) -> 00000000000000000000000000000000 @ \[15\]
14+
__CPROVER_pipe_count \(\) -> 00000000000000000000000000000000 @ \[11\]
15+
__CPROVER_malloc_size \(\) -> 0000000000000000000000000000000000000000000000000000000000000000 @ \[8\]
16+
__CPROVER_next_thread_id \(\) -> 0000000000000000000000000000000000000000000000000000000000000000 @ \[10\]
17+
__CPROVER_thread_id \(\) -> 0000000000000000000000000000000000000000000000000000000000000000 @ \[13\]
18+
do_variables#return_value \(\) -> TOP @ \[59\]
19+
main#return_value \(\) -> TOP @ \[1\]
20+
do_variables::1::bool_ \(\) -> TOP @ \[17\]
21+
do_variables::1::bool_1 \(\) -> TOP @ \[18\]
22+
do_variables::1::bool_2 \(\) -> TOP @ \[19\]
23+
do_variables::1::x \(\) -> TOP @ \[21\]
24+
global_x \(\) -> 00000000000000000000000000000101 @ \[20\]
25+
do_variables::1::x \(\) -> 00000000000000000000000000001010 @ \[22\]
26+
do_variables::1::y \(\) -> TOP @ \[23\]
27+
do_variables::1::y \(\) -> 00000000000000000000000000010100 @ \[24\]
28+
do_variables::1::x \(\) -> 00000000000000000000000000011110 @ \[25\]
29+
do_variables::1::y \(\) -> 00000000000000000000000000101000 @ \[26\]
30+
do_variables::1::y \(\) -> 00000000000000000000000000011110 @ \[27\]
31+
do_variables::1::x \(\) -> 00000000000000000000000000011110 @ \[28\]
32+
do_variables::1::x \(\) -> 00000000000000000000000000000101 @ \[29\]
33+
do_variables::1::x \(\) -> 00000000000000000000000000001111 @ \[30\]
34+
do_variables::1::y \(\) -> 00000000000000000000000000001010 @ \[31\]
35+
do_variables::1::x \(\) -> 00000000000000000000000000010100 @ \[33\]
36+
do_variables::1::x \(\) -> 00000000000000000000000000010100 @ \[33\, 35\]
37+
do_variables::1::x \(\) -> 00000000000000000000000000010100 @ \[33\, 35\]
38+
do_variables::1::x \(\) -> 00000000000000000000000000110010 @ \[37\]
39+
do_variables::1::x \(\) -> 00000000000000000000000000010100 @ \[39\]
40+
do_variables::1::x \(\) -> TOP @ \[39\, 41\]
41+
do_variables::1::x \(\) -> 00000000000000000000000000000000 @ \[43\]
42+
do_variables::1::x \(\) -> 00000000000000000000000000000011 @ \[45\]
43+
do_variables::1::x \(\) -> TOP @ \[45\, 47\]
44+
do_variables::1::x \(\) -> TOP @ \[45\, 47\, 50\]
45+
do_variables::1::y \(\) -> 00000000000000000000000000001010 @ \[52\]
46+
do_variables::1::x \(\) -> 00000000000000000000000000010100 @ \[53\]
47+
--

0 commit comments

Comments
 (0)