disproveJavaDataDepViaKeyAndJoanaGui/testdata/plusminusfalsepos.dispro at master · bigolol/disproveJavaDataDepViaKeyAndJoanaGui · GitHub

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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
{"path_to_jar" : "testdata/plusMinusFalsePositive/build/PlusMinusFalsePos.jar",
"path_to_java_source" : "testdata/plusMinusFalsePositive/",
"path_to_sdg" : "savedata/PlusMinusFalsePos3421557460184259452.pdg",
"state_saver" : {"formal_ins_to_pers_cg" : [
{ "sdg_node" : 49, "cg_node" : {"id" : 4, "cg_node_id" :9, "ir" : {

}}},
{ "sdg_node" : 50, "cg_node" : {"id" : 4, "cg_node_id" :9, "ir" : {

}}},
{ "sdg_node" : 51, "cg_node" : {"id" : 4, "cg_node_id" :9, "ir" : {

}}},
{ "sdg_node" : 68, "cg_node" : {"id" : 6, "cg_node_id" :11, "ir" : {

}}},
{ "sdg_node" : 69, "cg_node" : {"id" : 6, "cg_node_id" :11, "ir" : {

}}},
{ "sdg_node" : 40, "cg_node" : {"id" : 3, "cg_node_id" :8, "ir" : {

}}}],
"cgNodes" : [
{"id" : 0, "cg_node_id" :0, "ir" : {
"1" : "this"
}},
{"id" : 1, "cg_node_id" :0, "ir" : {

}},
{"id" : 2, "cg_node_id" :0, "ir" : {

}},
{"id" : 3, "cg_node_id" :8, "ir" : {

}},
{"id" : 4, "cg_node_id" :9, "ir" : {

}},
{"id" : 5, "cg_node_id" :0, "ir" : {
"1" : "this"
}},
{"id" : 6, "cg_node_id" :11, "ir" : {

}}],
"localPointerKeys" : [{"id" : 0, "value_number" : 1, "node" : 0
},
{"id" : 1, "value_number" : 1, "node" : 1
},
{"id" : 2, "value_number" : 1, "node" : 2
},
{"id" : 3, "value_number" : 1, "node" : 3
},
{"id" : 4, "value_number" : 1, "node" : 4
},
{"id" : 5, "value_number" : 1, "node" : 5
},
{"id" : 6, "value_number" : 1, "node" : 6
},
{"id" : 0, "value_number" : 1, "node" : 0
},
{"id" : 1, "value_number" : 1, "node" : 1
},
{"id" : 2, "value_number" : 1, "node" : 2
},
{"id" : 3, "value_number" : 1, "node" : 3
},
{"id" : 4, "value_number" : 1, "node" : 4
},
{"id" : 5, "value_number" : 1, "node" : 5
},
{"id" : 6, "value_number" : 1, "node" : 6
}],
"disjunctPointsTo" : []
},
"edges_methods_to_values" : {"formal_node_tuple_to_contract" : [{"in" : 69, "out" : 65, "contract" : "	/*@ requires true;	  @ determines \\result \\by this, l; */"}],"edge_to_loop_invariant_template" : [{"in" : 55, "out" : 56, "invariant" : "	/*	@ loop_invariant 	 	 @ assignable 	 	 @ determines \\result \\by this, l; 	 	 @ decreases */"}],"method_to_most_general_contract" : [{"method" : "PlusMinusFalsePos/identity/int,int", "most_general_contract" : "	/*@ requires true;	  @ determines this \\by this, l, h; */", }],"edge_to_loop_invariant" : [{"in" : 55, "out" : 56, "loop_invariants" : []}]},
"violation_wrapper" : {
"violations" : [],
"chops" : [
{
"src" : 11,
"sink" : 47,
"nodes_in_chop" : [
65,
50,
69,
70,
55,
71,
56,
72,
58,
11,
47]
}],
"summary_edges_sorted" : [
{"src" : 55, "sink" : 56}],
"summary_edges_methods": [
{"id" :0, "class_name" : "PlusMinusFalsePos", "method_name" : "identity", "arg_string" : "int,int"}],"summary_edges_chops" : [
{"pos" :0, "chops" : [
{"src" : 11, "sink" : 47}]}]
}}