Skip to content

Commit 91ebd42

Browse files
author
Lefan Zhang
authored
Merge pull request diffblue#2 from lefanz-amazon/lefan-abstraction
regression: add abst json files for some examples
2 parents 71a7f7d + 04a58ed commit 91ebd42

6 files changed

+237
-0
lines changed

‎regression/abstraction/aws_array_eq_c_str_ignore_case.json

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
{
2+
"entries": [
3+
{
4+
"entity": "array",
5+
"path": "aws_array_eq_c_str_ignore_case_harness.c/aws_array_eq_c_str_ignore_case_harness",
6+
"name": "c_str",
7+
"shape": {
8+
"indices": ["cncrt", "clast"],
9+
"assumptions": [
10+
"cncrt < clast"
11+
],
12+
"shape-type": "*c*c*"
13+
},
14+
"abst-functions":{
15+
"add-abs-conc": "./abst-funcs.c/add_abs_to_conc",
16+
"sub-abs-conc": "../abst-funcs.c/sub_conc_from_abs",
17+
"precise-check": "../abst-funcs.c/is_precise",
18+
"abstract-index": "../abst-funcs.c/two_abs",
19+
"concretize-index": "../abst-funcs.c/concretize",
20+
"multiply-indices": "none",
21+
"mod-indices": "none"
22+
},
23+
"related-entities": [
24+
{
25+
"entity": "array",
26+
"path": "aws_array_eq_c_str_ignore_case_harness.c/aws_array_eq_c_str_ignore_case_harness",
27+
"name": "array"
28+
},
29+
{
30+
"entity": "scalar",
31+
"path": "aws_array_eq_c_str_ignore_case_harness.c/aws_array_eq_c_str_ignore_case_harness",
32+
"name": "array_len"
33+
},
34+
{
35+
"entity": "scalar",
36+
"path": "aws_array_eq_c_str_ignore_case_harness.c/aws_array_eq_c_str_ignore_case_harness",
37+
"name": "str_len"
38+
}
39+
]
40+
41+
}
42+
]
43+
}

‎regression/abstraction/aws_array_eq_ignore_case.json

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
{
2+
"entries": [
3+
{
4+
"entity": "array",
5+
"path": "aws_array_eq_ignore_case_harness.c/aws_array_eq_ignore_case_harness",
6+
"name": "rhs",
7+
"shape": {
8+
"indices": ["cncrt"],
9+
"assumptions": [
10+
],
11+
"shape-type": "*c*"
12+
},
13+
"abst-functions":{
14+
"add-abs-conc": "./abst-funcs.c/add_abs_to_conc",
15+
"sub-abs-conc": "../abst-funcs.c/sub_conc_from_abs",
16+
"precise-check": "../abst-funcs.c/is_precise",
17+
"abstract-index": "../abst-funcs.c/one_abs",
18+
"concretize-index": "../abst-funcs.c/concretize",
19+
"multiply-indices": "none",
20+
"mod-indices": "none"
21+
},
22+
"related-entities": [
23+
{
24+
"entity": "array",
25+
"path": "aws_array_eq_ignore_case_harness.c/aws_array_eq_ignore_case_harness",
26+
"name": "lhs"
27+
},
28+
{
29+
"entity": "scalar",
30+
"path": "aws_array_eq_ignore_case_harness.c/aws_array_eq_ignore_case_harness",
31+
"name": "rhs_len"
32+
},
33+
{
34+
"entity": "scalar",
35+
"path": "aws_array_eq_ignore_case_harness.c/aws_array_eq_ignore_case_harness",
36+
"name": "lhs_len"
37+
}
38+
]
39+
40+
}
41+
]
42+
}

‎regression/abstraction/aws_array_list_comparator_string.json

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
{
2+
"entries": [
3+
{
4+
"entity": "array",
5+
"path": "aws_array_list_comparator_string_harness.c/aws_array_list_comparator_string_harness",
6+
"name": "str_a->bytes",
7+
"shape": {
8+
"indices": ["cncrt"],
9+
"assumptions": [
10+
],
11+
"shape-type": "*c*"
12+
},
13+
"abst-functions":{
14+
"add-abs-conc": "./abst-funcs.c/add_abs_to_conc",
15+
"sub-abs-conc": "../abst-funcs.c/sub_conc_from_abs",
16+
"precise-check": "../abst-funcs.c/is_precise",
17+
"abstract-index": "../abst-funcs.c/one_abs",
18+
"concretize-index": "../abst-funcs.c/concretize",
19+
"multiply-indices": "none",
20+
"mod-indices": "none"
21+
},
22+
"related-entities": [
23+
{
24+
"entity": "array",
25+
"path": "aws_array_list_comparator_string_harness.c/aws_array_list_comparator_string_harness",
26+
"name": "str_b->bytes"
27+
},
28+
{
29+
"entity": "scalar",
30+
"path": "aws_array_list_comparator_string_harness.c/aws_array_list_comparator_string_harness",
31+
"name": "str_a->len"
32+
},
33+
{
34+
"entity": "scalar",
35+
"path": "aws_array_list_comparator_string_harness.c/aws_array_list_comparator_string_harness",
36+
"name": "str_b->len"
37+
}
38+
]
39+
40+
}
41+
]
42+
}

‎regression/abstraction/aws_array_list_front.json

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
{
2+
"entries": [
3+
{
4+
"entity": "array",
5+
"path": "aws_array_list_front_harness.c/aws_array_list_front_harness",
6+
"name": "list->data",
7+
"shape": {
8+
"indices": ["front", "cncrt"],
9+
"assumptions": [
10+
"front < cncrt",
11+
"front = 0"
12+
],
13+
"shape-type": "c*c*"
14+
},
15+
"abst-functions":{
16+
"add-abs-conc": "./abst-funcs.c/add_abs_to_conc",
17+
"sub-abs-conc": "../abst-funcs.c/sub_conc_from_abs",
18+
"precise-check": "../abst-funcs.c/is_precise",
19+
"abstract-index": "../abst-funcs.c/two_abs",
20+
"concretize-index": "../abst-funcs.c/concretize",
21+
"multiply-indices": "none",
22+
"mod-indices": "none"
23+
},
24+
"related-entities": [
25+
{
26+
"entity": "scalar",
27+
"path": "aws_array_list_front_harness.c/aws_array_list_front_harness",
28+
"name": "list->length"
29+
}
30+
]
31+
32+
}
33+
]
34+
}

‎regression/abstraction/aws_array_list_get_at.json

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
{
2+
"entries": [
3+
{
4+
"entity": "array",
5+
"path": "aws_array_list_get_at_harness.c/aws_array_list_get_at_harness",
6+
"name": "list->data",
7+
"shape": {
8+
"indices": ["c0", "c1"],
9+
"assumptions": [
10+
"c0 < c1"
11+
],
12+
"shape-type": "*c*c*"
13+
},
14+
"abst-functions":{
15+
"add-abs-conc": "./abst-funcs.c/add_abs_to_conc",
16+
"sub-abs-conc": "../abst-funcs.c/sub_conc_from_abs",
17+
"precise-check": "../abst-funcs.c/is_precise",
18+
"abstract-index": "../abst-funcs.c/two_abs",
19+
"concretize-index": "../abst-funcs.c/concretize",
20+
"multiply-indices": "none",
21+
"mod-indices": "none"
22+
},
23+
"related-entities": [
24+
{
25+
"entity": "scalar",
26+
"path": "aws_array_list_get_at_harness.c/aws_array_list_get_at_harness",
27+
"name": "list->length"
28+
}
29+
]
30+
31+
}
32+
]
33+
}

‎regression/abstraction/aws_array_list_pop_back.json

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
{
2+
"entries": [
3+
{
4+
"entity": "array",
5+
"path": "aws_array_list_pop_back_harness.c/aws_array_list_pop_back_harness",
6+
"name": "list->data",
7+
"shape": {
8+
"indices": ["c0", "c1"],
9+
"assumptions": [
10+
"c0 = c1-1"
11+
],
12+
"shape-type": "*cc*"
13+
},
14+
"abst-functions":{
15+
"add-abs-conc": "./abst-funcs.c/add_abs_to_conc",
16+
"sub-abs-conc": "../abst-funcs.c/sub_conc_from_abs",
17+
"precise-check": "../abst-funcs.c/is_precise",
18+
"abstract-index": "../abst-funcs.c/two_abs",
19+
"concretize-index": "../abst-funcs.c/concretize",
20+
"multiply-indices": "none",
21+
"mod-indices": "none"
22+
},
23+
"related-entities": [
24+
{
25+
"entity": "array",
26+
"path": "aws_array_list_pop_back_harness.c/aws_array_list_pop_back_harness",
27+
"name": "old->data"
28+
},
29+
{
30+
"entity": "scalar",
31+
"path": "aws_array_list_pop_back_harness.c/aws_array_list_pop_back_harness",
32+
"name": "old->length"
33+
},
34+
{
35+
"entity": "scalar",
36+
"path": "aws_array_list_pop_back_harness.c/aws_array_list_pop_back_harness",
37+
"name": "list->length"
38+
}
39+
]
40+
41+
}
42+
]
43+
}

0 commit comments

Comments
 (0)