Skip to content

Commit ef2b0a0

Browse files
cristina-davidcristina-david
authored
Merge pull request #12 from peterschrammel/test_gen
Sync json output fixes
2 parents ff1e5c6 + ac97282 commit ef2b0a0

File tree

136 files changed

+2430
-237
lines changed

Some content is hidden

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

136 files changed

+2430
-237
lines changed

‎regression/cbmc-java/LocalVarTable2/LocalVarTable2.class

952 Bytes
Binary file not shown.

‎regression/cbmc-java/LocalVarTable2/LocalVarTable2.java

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
// Must compile this with -g (produces LocalVarTable) to exhibit bug.
2+
3+
public class LocalVarTable2 {
4+
5+
public static Object f() {
6+
for(int i = 0; i < 10; ++i) { System.out.printf("Count %d\n", i); }
7+
try {
8+
return new Object();
9+
}
10+
finally {
11+
System.out.println("Finally executed\n");
12+
}
13+
}
14+
15+
public static void main(String[] args) {
16+
f();
17+
}
18+
19+
}

‎regression/cbmc-java/LocalVarTable2/test.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
LocalVarTable2.class
3+
--show-goto-functions
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
return_value.*(void \*)i

‎regression/cbmc-java/virtual5/child.class

229 Bytes
Binary file not shown.

‎regression/cbmc-java/virtual5/parent.class

240 Bytes
Binary file not shown.

‎regression/cbmc-java/virtual5/test.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
virtual5.class
3+
--function virtual5.test
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$

‎regression/cbmc-java/virtual5/virtual5.class

574 Bytes
Binary file not shown.

‎regression/cbmc-java/virtual5/virtual5.java

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
public class virtual5 {
2+
3+
public static void test(parent p, child c) {
4+
5+
if(p==null)
6+
return;
7+
assert(p.get()==1);
8+
9+
}
10+
11+
}
12+
13+
class parent {
14+
15+
public int get() { return 1; }
16+
17+
}
18+
19+
class child extends parent {
20+
21+
public int get() { return 2; }
22+
23+
}

‎regression/cegis/cegis_jsa_benchmark_00/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ int main(void)
2525
while (__CPROVER_jsa_hasNext(&heap, __CPROVER_jsa_iterator_it))
2626
{
2727
const __CPROVER_jsa_data_t el=__CPROVER_jsa_next(&heap, __CPROVER_jsa_iterator_it);
28-
if (i % 2 == 0)
28+
if (__CPROVER_jsa_mod(i, 2) == 0)
2929
{
3030
__CPROVER_jsa_remove(&heap, __CPROVER_jsa_iterator_it);
3131
}

‎regression/cegis/cegis_jsa_benchmark_07/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ int main(void)
2525
__CPROVER_jsa_hasNext(&heap, __CPROVER_jsa_iterator_it);)
2626
{
2727
const __CPROVER_jsa_data_t num=__CPROVER_jsa_next(&heap, __CPROVER_jsa_iterator_it);
28-
if (num%2 == 0)
28+
if (__CPROVER_jsa_mod(num, 2) == 0)
2929
{
3030
__CPROVER_jsa_remove(&heap, __CPROVER_jsa_iterator_it);
3131
}

‎regression/cegis/cegis_jsa_benchmark_09/main.c

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
21
#ifdef __CPROVER
32
#define __CPROVER_JSA_MAX_CONCRETE_NODES 1u
43
#define __CPROVER_JSA_MAX_ABSTRACT_NODES 0u
@@ -25,7 +24,7 @@ int main(void)
2524
while (__CPROVER_jsa_hasNext(&heap, __CPROVER_jsa_iterator_it))
2625
{
2726
const __CPROVER_jsa_data_t i=__CPROVER_jsa_next(&heap, __CPROVER_jsa_iterator_it);
28-
if (i % 2 == 0)
27+
if (__CPROVER_jsa_mod(i, 2) == 0)
2928
{
3029
__CPROVER_jsa_remove(&heap, __CPROVER_jsa_iterator_it);
3130
}

‎regression/cegis/cegis_jsa_benchmark_12/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ int main(void)
2525
while (__CPROVER_jsa_hasNext(&heap, __CPROVER_jsa_iterator_it))
2626
{
2727
const __CPROVER_jsa_data_t i=__CPROVER_jsa_next(&heap, __CPROVER_jsa_iterator_it);
28-
if (i % 2 == 0)
28+
if (__CPROVER_jsa_mod(i, 2) == 0)
2929
{
3030
__CPROVER_jsa_remove(&heap, __CPROVER_jsa_iterator_it);
3131
}

‎regression/cegis/cegis_jsa_benchmark_15/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ int main(void)
2525
while (__CPROVER_jsa_hasNext(&heap, __CPROVER_jsa_iterator_it))
2626
{
2727
const __CPROVER_jsa_data_t i=__CPROVER_jsa_next(&heap, __CPROVER_jsa_iterator_it);
28-
if (i % 2 == 0)
28+
if (__CPROVER_jsa_mod(i, 2) == 0)
2929
{
3030
__CPROVER_jsa_remove(&heap, __CPROVER_jsa_iterator_it);
3131
}

‎regression/cegis/cegis_jsa_benchmark_18/main.c

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
11
#ifdef __CPROVER
2-
#define __CPROVER_JSA_MAX_CONCRETE_NODES 2u
3-
#define __CPROVER_JSA_MAX_NODES_PER_LIST 1u
2+
#define __CPROVER_JSA_MAX_CONCRETE_NODES 3u
3+
#define __CPROVER_JSA_MAX_NODES_PER_CE_LIST 1u
44
#define __CPROVER_JSA_MAX_ABSTRACT_NODES 0u
55
#define __CPROVER_JSA_MAX_ITERATORS 1u
66
#define __CPROVER_JSA_MAX_LISTS 2u
77

88
#define JSA_SYNTHESIS_H_
99
#define __CPROVER_JSA_DEFINE_TRANSFORMERS
10-
#define __CPROVER_JSA_MAX_QUERY_SIZE 2u
10+
#define __CPROVER_JSA_MAX_QUERY_SIZE 3u
1111
#define __CPROVER_JSA_MAX_PRED_SIZE 1u
1212
#define __CPROVER_JSA_NUM_PRED_OPS 5u
1313
#define __CPROVER_JSA_NUM_PRED_RESULT_OPS 2u

‎regression/cegis/cegis_jsa_benchmark_18_02/main.c

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
#ifdef __CPROVER
2-
#define __CPROVER_JSA_MAX_CONCRETE_NODES 2u
3-
#define __CPROVER_JSA_MAX_NODES_PER_LIST 1u
2+
#define __CPROVER_JSA_MAX_CONCRETE_NODES 3u
3+
#define __CPROVER_JSA_MAX_NODES_PER_CE_LIST 1u
44
#define __CPROVER_JSA_MAX_ABSTRACT_NODES 0u
55
#define __CPROVER_JSA_MAX_ITERATORS 1u
66
#define __CPROVER_JSA_MAX_LISTS 2u
77

88
#define JSA_SYNTHESIS_H_
99
#define __CPROVER_JSA_DEFINE_TRANSFORMERS
1010
#define __CPROVER_JSA_MAX_QUERY_SIZE 3u
11-
#define __CPROVER_JSA_MAX_PRED_SIZE 1u
11+
#define __CPROVER_JSA_MAX_PRED_SIZE 2u
1212
#define __CPROVER_JSA_NUM_PRED_OPS 5u
1313
#define __CPROVER_JSA_NUM_PRED_RESULT_OPS 2u
1414
#endif

‎regression/cegis/cegis_jsa_benchmark_20/main.c

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
11
#ifdef __CPROVER
2-
#define __CPROVER_JSA_MAX_CONCRETE_NODES 2u
3-
#define __CPROVER_JSA_MAX_NODES_PER_LIST 1u
2+
#define __CPROVER_JSA_MAX_CONCRETE_NODES 3u
3+
#define __CPROVER_JSA_MAX_NODES_PER_CE_LIST 1u
44
#define __CPROVER_JSA_MAX_ABSTRACT_NODES 0u
55
#define __CPROVER_JSA_MAX_ITERATORS 1u
66
#define __CPROVER_JSA_MAX_LISTS 2u
77

88
#define JSA_SYNTHESIS_H_
99
#define __CPROVER_JSA_DEFINE_TRANSFORMERS
10-
#define __CPROVER_JSA_MAX_QUERY_SIZE 2u
10+
#define __CPROVER_JSA_MAX_QUERY_SIZE 3u
1111
#define __CPROVER_JSA_MAX_PRED_SIZE 1u
1212
#define __CPROVER_JSA_NUM_PRED_OPS 4u
1313
#define __CPROVER_JSA_NUM_PRED_RESULT_OPS 2u

‎regression/cegis/cegis_jsa_benchmark_24/main.c

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,8 @@
77
#define JSA_SYNTHESIS_H_
88
#define __CPROVER_JSA_DEFINE_TRANSFORMERS
99
#define __CPROVER_JSA_MAX_QUERY_SIZE 2u
10-
#define __CPROVER_JSA_MAX_PRED_SIZE 2u
11-
#define __CPROVER_JSA_NUM_PRED_OPS 7u
10+
#define __CPROVER_JSA_MAX_PRED_SIZE 3u
11+
#define __CPROVER_JSA_NUM_PRED_OPS 5u
1212
#define __CPROVER_JSA_NUM_PRED_RESULT_OPS 2u
1313
#endif
1414

@@ -20,13 +20,11 @@ int main(void)
2020
__CPROVER_jsa_assume_valid_heap(&heap);
2121
const __CPROVER_jsa_list_id_t __CPROVER_jsa_list_l;
2222
__CPROVER_jsa_assume_valid_list(&heap, __CPROVER_jsa_list_l);
23-
const __CPROVER_jsa_word_t two=2u;
24-
const __CPROVER_jsa_word_t zero=0u;
2523
for (const __CPROVER_jsa_iterator_id_t __CPROVER_jsa_iterator_it=__CPROVER_jsa_iterator(&heap, __CPROVER_jsa_list_l);
2624
__CPROVER_jsa_hasNext(&heap, __CPROVER_jsa_iterator_it);)
2725
{
2826
const __CPROVER_jsa_word_t x=__CPROVER_jsa_next(&heap, __CPROVER_jsa_iterator_it);
29-
if(x % two == zero)
27+
if(__CPROVER_jsa_mod(x, 2) == 0)
3028
{
3129
__CPROVER_jsa_set(&heap, __CPROVER_jsa_iterator_it, 0);
3230
}

‎regression/cegis/cegis_jsa_benchmark_28/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ int main(void)
2424
__CPROVER_jsa_hasNext(&heap, __CPROVER_jsa_iterator_it);)
2525
{
2626
const __CPROVER_jsa_data_t value=__CPROVER_jsa_next(&heap, __CPROVER_jsa_iterator_it);
27-
if (value % 2u == 1u)
27+
if (__CPROVER_jsa_mod(value, 2u) == 1u)
2828
{
2929
__CPROVER_jsa_remove(&heap, __CPROVER_jsa_iterator_it);
3030
}

‎regression/cegis/cegis_jsa_benchmark_30/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ int main(void)
2424
__CPROVER_jsa_hasNext(&heap, __CPROVER_jsa_iterator_it);)
2525
{
2626
const __CPROVER_jsa_data_t i=__CPROVER_jsa_next(&heap, __CPROVER_jsa_iterator_it);
27-
if (i % 2 == 0)
27+
if (__CPROVER_jsa_mod(i, 2) == 0)
2828
{
2929
__CPROVER_jsa_remove(&heap, __CPROVER_jsa_iterator_it);
3030
}

‎regression/cegis/cegis_jsa_benchmark_31/main.c

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
11
#ifdef __CPROVER
2-
#define __CPROVER_JSA_MAX_CONCRETE_NODES 2u
3-
#define __CPROVER_JSA_MAX_NODES_PER_LIST 1u
2+
#define __CPROVER_JSA_MAX_CONCRETE_NODES 3u
3+
#define __CPROVER_JSA_MAX_NODES_PER_CE_LIST 1u
44
#define __CPROVER_JSA_MAX_ABSTRACT_NODES 0u
55
#define __CPROVER_JSA_MAX_ITERATORS 1u
66
#define __CPROVER_JSA_MAX_LISTS 2u
77

88
#define JSA_SYNTHESIS_H_
99
#define __CPROVER_JSA_DEFINE_TRANSFORMERS
10-
#define __CPROVER_JSA_MAX_QUERY_SIZE 2u
10+
#define __CPROVER_JSA_MAX_QUERY_SIZE 3u
1111
#define __CPROVER_JSA_MAX_PRED_SIZE 2u
1212
#define __CPROVER_JSA_NUM_PRED_OPS 5u
1313
#define __CPROVER_JSA_NUM_PRED_RESULT_OPS 2u

‎regression/cegis/cegis_jsa_benchmark_32/GenPrime.java

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
package com.hackerrank.test;
2+
3+
import java.util.ArrayList;
4+
import java.util.List;
5+
6+
public class GenPrime {
7+
public static void main(String[] args) {
8+
int pp = 2;
9+
List<Integer> ps = new ArrayList<Integer>();
10+
ps.add(pp);
11+
int limit = 100;
12+
while (pp < limit){
13+
pp+=1;
14+
for (Integer integer : ps) {
15+
if(pp%integer == 0)
16+
break;
17+
else
18+
ps.add(pp);
19+
}
20+
21+
}
22+
for (Integer integer : ps) {
23+
System.out.println(integer);
24+
}
25+
}
26+
}

‎regression/cegis/cegis_jsa_benchmark_32/main.c

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
#ifdef __CPROVER
2+
#define __CPROVER_JSA_MAX_CONCRETE_NODES 2u
3+
#define __CPROVER_JSA_MAX_NODES_PER_CE_LIST 1u
4+
#define __CPROVER_JSA_MAX_ABSTRACT_NODES 0u
5+
#define __CPROVER_JSA_MAX_ITERATORS 1u
6+
#define __CPROVER_JSA_MAX_LISTS 1u
7+
8+
#define JSA_SYNTHESIS_H_
9+
#define __CPROVER_JSA_DEFINE_TRANSFORMERS
10+
#define __CPROVER_JSA_MAX_QUERY_SIZE 2u
11+
#define __CPROVER_JSA_MAX_PRED_SIZE 1u
12+
#define __CPROVER_JSA_NUM_PRED_OPS 4u
13+
#define __CPROVER_JSA_NUM_PRED_RESULT_OPS 2u
14+
#endif
15+
16+
#include "../../../src/ansi-c/library/jsa.h"
17+
18+
int main(void)
19+
{
20+
__CPROVER_jsa_abstract_heapt heap;
21+
__CPROVER_jsa_assume_valid_heap(&heap);
22+
const __CPROVER_jsa_list_id_t __CPROVER_jsa_list_ps;
23+
__CPROVER_jsa_assume_valid_list(&heap, __CPROVER_jsa_list_ps);
24+
const __CPROVER_jsa_data_t pp;
25+
const __CPROVER_jsa_iterator_id_t __CPROVER_jsa_iterator_it=__CPROVER_jsa_iterator(&heap, __CPROVER_jsa_list_ps);
26+
for (;__CPROVER_jsa_hasNext(&heap, __CPROVER_jsa_iterator_it);)
27+
{
28+
const __CPROVER_jsa_data_t integer=__CPROVER_jsa_next(&heap, __CPROVER_jsa_iterator_it);
29+
if(__CPROVER_jsa_mod(pp, integer) == 0)
30+
break;
31+
else
32+
__CPROVER_jsa_add(&heap, __CPROVER_jsa_list_ps, pp);
33+
}
34+
35+
return 0;
36+
}

‎regression/cegis/cegis_jsa_benchmark_32/source.url

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
https://raw.githubusercontent.com/vvkalkundri/hacker/fb4eb7917a9c311048d5962b816113c347f4067a/HackerRank/src/com/hackerrank/test/GenPrime.java

‎regression/cegis/cegis_jsa_benchmark_32/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
7+
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
8+
--
9+
^warning: ignoring

‎regression/cegis/cegis_jsa_benchmark_33/T1E3R.java

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
package naivePrimeGeneration;
2+
3+
import java.util.ArrayList;
4+
import java.util.List;
5+
6+
public class T1E3R {
7+
8+
public static List<Integer> source(int max) {
9+
List<Integer> primes = new ArrayList<Integer>();
10+
OUTERLOOP: for (int i = 2; i <= max; i++) {
11+
for (Integer p : primes)
12+
if (i / p != 0)
13+
break OUTERLOOP;
14+
primes.add(i);
15+
}
16+
return primes;
17+
}
18+
19+
public static List<Integer> target(int max) {
20+
List<Integer> primes = new ArrayList<Integer>();
21+
OUTERLOOP: for (int i = 2; i <= max; i++) {
22+
for (Integer p : primes)
23+
if (i % p == 0)
24+
continue OUTERLOOP;
25+
primes.add(i);
26+
}
27+
return primes;
28+
}
29+
30+
}
31+
/*
32+
* Actual differences: None
33+
*
34+
* Expected difference score: 0.0
35+
*
36+
* Expected recommended edits: 6: None
37+
*/

‎regression/cegis/cegis_jsa_benchmark_33/main.c

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
#ifdef __CPROVER
2+
#define __CPROVER_JSA_MAX_CONCRETE_NODES 1u
3+
#define __CPROVER_JSA_MAX_ABSTRACT_NODES 0u
4+
#define __CPROVER_JSA_MAX_ITERATORS 1u
5+
#define __CPROVER_JSA_MAX_LISTS 1u
6+
7+
#define JSA_SYNTHESIS_H_
8+
#define __CPROVER_JSA_DEFINE_TRANSFORMERS
9+
#define __CPROVER_JSA_MAX_QUERY_SIZE 2u
10+
#define __CPROVER_JSA_MAX_PRED_SIZE 1u
11+
#define __CPROVER_JSA_NUM_PRED_OPS 4u
12+
#define __CPROVER_JSA_NUM_PRED_RESULT_OPS 2u
13+
#endif
14+
15+
#include "../../../src/ansi-c/library/jsa.h"
16+
17+
int main(void)
18+
{
19+
__CPROVER_jsa_abstract_heapt heap;
20+
__CPROVER_jsa_assume_valid_heap(&heap);
21+
const __CPROVER_jsa_list_id_t __CPROVER_jsa_list_ps;
22+
__CPROVER_jsa_assume_valid_list(&heap, __CPROVER_jsa_list_ps);
23+
const __CPROVER_jsa_data_t i;
24+
const __CPROVER_jsa_iterator_id_t __CPROVER_jsa_iterator_it=__CPROVER_jsa_iterator(&heap, __CPROVER_jsa_list_ps);
25+
for (;__CPROVER_jsa_hasNext(&heap, __CPROVER_jsa_iterator_it);)
26+
{
27+
const __CPROVER_jsa_data_t p=__CPROVER_jsa_next(&heap, __CPROVER_jsa_iterator_it);
28+
// Transformed "find" to "filter" to accommodate front-end restrictions.
29+
if (__CPROVER_jsa_div(i, p) == 0)
30+
{
31+
__CPROVER_jsa_remove(&heap, __CPROVER_jsa_iterator_it);
32+
}
33+
}
34+
35+
return 0;
36+
}

‎regression/cegis/cegis_jsa_benchmark_33/source.url

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
https://raw.githubusercontent.com/kurtisz/ASTRecognition/bb379b75c10979645b6822fe9dd012341a0ff409/TestWorkspace/Tests/src/naivePrimeGeneration/T1E3R.java

‎regression/cegis/cegis_jsa_benchmark_33/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
7+
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
8+
--
9+
^warning: ignoring

0 commit comments

Comments
 (0)