Skip to content

Commit 1ffb76a

Browse files
cristina-davidcristina-david
authored
Merge pull request #11 from smowton/test_gen_mocks
Miscellany
2 parents 9ebc7d3 + 1dccdec commit 1ffb76a

File tree

110 files changed

+2324
-887
lines changed

Some content is hidden

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

110 files changed

+2324
-887
lines changed

‎regression/ansi-c/Universal_characters1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

44
^EXIT=0$

‎regression/cbmc-concurrency/norace_array1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33

44
^EXIT=0$

‎regression/cbmc-concurrency/norace_struct1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33

44
^EXIT=0$

‎regression/cbmc-cover/branch2/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.coverage.1\] file main.c line 5 function main function main entry point: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 6 function main function main block 2 branch false: SATISFIED$
8-
^\[main.coverage.3\] file main.c line 6 function main function main block 2 branch true: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 6 function main function main block 3 branch false: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 6 function main function main block 3 branch true: SATISFIED$
99
--
1010
^warning: ignoring

‎regression/cbmc-cover/mcdc3/main.c

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,10 @@
11
int main()
22
{
33
unsigned x, y;
4+
5+
__CPROVER_input("x", x);
6+
__CPROVER_input("y", y);
7+
48
if (!(x>3) && y<5)
59
;
610

‎regression/cbmc-cover/mcdc3/test.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ main.c
33
--cover mcdc
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 4 function main MC/DC independence condition `!(x > (unsigned int)3) && !(y < (unsigned int)5).*: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 4 function main MC/DC independence condition `y < (unsigned int)5 && !(x > (unsigned int)3).*: SATISFIED$
8-
^\[main.coverage.3\] file main.c line 4 function main MC/DC independence condition `y < (unsigned int)5 && x > (unsigned int)3.*: SATISFIED$
6+
^\[main.coverage.1\] file main.c line 8 function main MC/DC independence condition `!(x > (unsigned int)3) && !(y < (unsigned int)5).*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition `y < (unsigned int)5 && !(x > (unsigned int)3).*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 8 function main MC/DC independence condition `y < (unsigned int)5 && x > (unsigned int)3.*: SATISFIED$
99
^\*\* .* of .* covered (100.0%)$
1010
^\*\* Used 4 iterations$
1111
--

‎regression/cbmc-cover/mcdc6/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
int main()
22
{
33
unsigned x;
4+
5+
__CPROVER_input("x", x);
6+
47
if(x<3)
58
;
69

‎regression/cbmc-cover/mcdc6/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ main.c
33
--cover mcdc
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 4 function main decision/condition `x < (unsigned int)3.* false: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 4 function main decision/condition `x < (unsigned int)3.* true: SATISFIED$
6+
^\[main.coverage.1\] file main.c line 7 function main decision/condition `x < (unsigned int)3.* false: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 7 function main decision/condition `x < (unsigned int)3.* true: SATISFIED$
88
^\*\* .* of .* covered (100.0%)$
99
^\*\* Used 2 iterations$
1010
--

‎regression/cbmc-cover/mcdc7/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
int main()
22
{
33
signed x, y;
4+
5+
__CPROVER_input("x", x);
6+
__CPROVER_input("y", y);
47

58
y = x*123<0 ? 0 : (x*123>100 ? 100 : x*123 );
69

‎regression/cbmc-cover/mcdc7/test.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ main.c
33
--cover mcdc
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 5 function main decision/condition `x \* 123 > 100.* false: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 5 function main decision/condition `x \* 123 > 100.* true: SATISFIED$
8-
^\[main.coverage.3\] file main.c line 5 function main decision/condition `x \* 123 < 0.* false: SATISFIED$
9-
^\[main.coverage.4\] file main.c line 5 function main decision/condition `x \* 123 < 0.* true: SATISFIED$
6+
^\[main.coverage.1\] file main.c line 8 function main decision/condition `x \* 123 > 100.* false: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 8 function main decision/condition `x \* 123 > 100.* true: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 8 function main decision/condition `x \* 123 < 0.* false: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 8 function main decision/condition `x \* 123 < 0.* true: SATISFIED$
1010
^\*\* .* of .* covered (100.0%)$
1111
^\*\* Used 2 iterations$
1212
--

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
Main.class
33
--all-properties
44
^EXIT=10$

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
Main.class
33
--function "A.dummy:()V"
44
^EXIT=0$

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

146 Bytes
Binary file not shown.

‎regression/cbmc-java/monitorenter1/monitorenter1.java

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,18 @@
11
public class monitorenter1
22
{
3-
public boolean doIt(boolean b)
3+
public int doIt(int what)
44
{
5-
boolean a;
5+
int some;
6+
67
synchronized(this) {
7-
a = !b;
8+
some=what;
89
}
9-
return a;
10+
11+
return some;
1012
}
1113

1214
public void test()
1315
{
14-
assert doIt(false);
16+
assert doIt(1)==1;
1517
}
1618
}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
KNOWNBUG
2-
virtual1.class
1+
CORE
2+
monitorenter1.class
33
--function monitorenter1.test
44
^EXIT=0$
55
^SIGNAL=0$

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ package_friendly1.class package_friendly2.class --show-goto-functions
44
^main[.]main[(][)].*$
55
^package_friendly1[.]operation1[(][)].*$
66
^package_friendly2[.]operation2[(][)].*$
7-
^EXIT=6$
7+
^EXIT=0$
88
^SIGNAL=0$
99
--
1010
^warning: ignoring

‎regression/cegis/cegis_jsa_benchmark_18/main.c

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,10 +28,8 @@ int main(void)
2828
__CPROVER_jsa_hasNext(&heap, __CPROVER_jsa_iterator_it);)
2929
{
3030
const __CPROVER_jsa_data_t integer=__CPROVER_jsa_next(&heap, __CPROVER_jsa_iterator_it);
31-
//if ((integer - min) > 0)
3231
if (integer > min)
3332
{
34-
//__CPROVER_jsa_add(&heap, __CPROVER_jsa_list_newList, integer - min);
3533
__CPROVER_jsa_add(&heap, __CPROVER_jsa_list_newList, integer);
3634
}
3735
}

‎regression/cegis/cegis_jsa_benchmark_31/ArrayUtils.java

Lines changed: 80 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,80 @@
1+
package arrays;
2+
3+
import java.util.ArrayList;
4+
import java.util.Arrays;
5+
import java.util.List;
6+
7+
8+
9+
public class ArrayUtils {
10+
11+
public Integer[] merge(Integer[] array1, Integer[] array2){
12+
13+
List<Integer> returnedList = new ArrayList<Integer>();
14+
List<Integer> concatList = array1 != null ? new ArrayList<Integer>(Arrays.asList(array1)) :
15+
(array2 != null ? new ArrayList<Integer>(Arrays.asList(array2)) : new ArrayList<Integer>()) ;
16+
if(array2 != null && array2 != null)
17+
concatList.addAll(Arrays.asList(array2));
18+
19+
for(Integer element2: concatList){
20+
21+
if(returnedList.indexOf(element2) == -1){
22+
returnedList.add(element2);
23+
}
24+
25+
}
26+
return (Integer[]) returnedList.toArray(new Integer[returnedList.size()]);
27+
}
28+
29+
public Integer[] innerJoin(Integer[] array1, Integer[] array2){
30+
31+
List<Integer> returnedList = new ArrayList<Integer>();
32+
33+
for(Integer element1: array1){
34+
35+
for(Integer element2: array2){
36+
if(element2 == element1){
37+
returnedList.add(element1);
38+
break;
39+
}
40+
}
41+
}
42+
43+
return (Integer[]) returnedList.toArray(new Integer[returnedList.size()]);
44+
}
45+
46+
public Integer[] leftJoin(Integer[] array1, Integer[] array2){
47+
48+
List<Integer> returnedList = array1 != null ? new ArrayList<Integer>(Arrays.asList(array1)) :
49+
(array2 != null ? new ArrayList<Integer>(Arrays.asList(array2)) :
50+
new ArrayList<Integer>());
51+
if(array1 != null){
52+
for(Integer element2: array2){
53+
54+
if(returnedList.indexOf(element2) > -1){
55+
returnedList.add(element2);
56+
}
57+
}
58+
}
59+
60+
return (Integer[]) returnedList.toArray(new Integer[returnedList.size()]);
61+
}
62+
63+
public Integer[] outerJoin(Integer[] array1, Integer[] array2){
64+
65+
List<Integer> returnedList = new ArrayList<Integer>();
66+
List<Integer> concatList = array1 != null ? new ArrayList<Integer>(Arrays.asList(array1)) :
67+
(array2 != null ? new ArrayList<Integer>(Arrays.asList(array2)) : new ArrayList<Integer>()) ;
68+
if(array1 != null && array2 != null)
69+
concatList.addAll(Arrays.asList(array2));
70+
71+
for(Integer element1: concatList){
72+
if(concatList.indexOf(element1) == concatList.lastIndexOf(element1)){
73+
returnedList.add(element1);
74+
}
75+
}
76+
77+
return (Integer[]) returnedList.toArray(new Integer[returnedList.size()]);
78+
}
79+
80+
}

‎regression/cegis/cegis_jsa_benchmark_31/main.c

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
#ifdef __CPROVER
2+
#define __CPROVER_JSA_MAX_CONCRETE_NODES 2u
3+
#define __CPROVER_JSA_MAX_NODES_PER_LIST 1u
4+
#define __CPROVER_JSA_MAX_ABSTRACT_NODES 0u
5+
#define __CPROVER_JSA_MAX_ITERATORS 1u
6+
#define __CPROVER_JSA_MAX_LISTS 2u
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 2u
12+
#define __CPROVER_JSA_NUM_PRED_OPS 5u
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_input=0;
23+
__CPROVER_jsa_assume_valid_list(&heap, __CPROVER_jsa_list_input);
24+
const __CPROVER_jsa_list_id_t __CPROVER_jsa_list_returnedList=1;
25+
__CPROVER_jsa_assume_new_list(&heap, __CPROVER_jsa_list_returnedList);
26+
const __CPROVER_jsa_data_t element1;
27+
for (const __CPROVER_jsa_iterator_id_t __CPROVER_jsa_iterator_it=__CPROVER_jsa_iterator(&heap, __CPROVER_jsa_list_input);
28+
__CPROVER_jsa_hasNext(&heap, __CPROVER_jsa_iterator_it);)
29+
{
30+
const __CPROVER_jsa_data_t element2=__CPROVER_jsa_next(&heap, __CPROVER_jsa_iterator_it);
31+
if (element2 == element1)
32+
{
33+
__CPROVER_jsa_add(&heap, __CPROVER_jsa_list_returnedList, element2);
34+
}
35+
}
36+
37+
return 0;
38+
}

‎regression/cegis/cegis_jsa_benchmark_31/source.url

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
https://raw.githubusercontent.com/Vladimir-Moskov/GitJavaProjects/f12fc8219bb5b7ad53c4af753d32594cab20138e/javaJunior/src/arrays/ArrayUtils.java

‎regression/cegis/cegis_jsa_benchmark_31/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/fault-localization/Makefile

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
default: tests.log
2+
3+
test:
4+
@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
5+
../failed-tests-printer.pl ; \
6+
exit 1 ; \
7+
fi
8+
9+
tests.log: ../test.pl
10+
@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
11+
../failed-tests-printer.pl ; \
12+
exit 1 ; \
13+
fi
14+
15+
show:
16+
@for dir in *; do \
17+
if [ -d "$$dir" ]; then \
18+
vim -o "$$dir/*.c" "$$dir/*.out"; \
19+
fi; \
20+
done;

‎regression/fault-localization/all_properties1/main.c

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#include <assert.h>
2+
3+
void main()
4+
{
5+
int x, c;
6+
if(c) x=0;
7+
else x++;
8+
assert(x==0);
9+
assert(x!=0);
10+
}

‎regression/fault-localization/all_properties1/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+
--localize-faults
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
line 7 function main$
7+
line 6 function main$
8+
^VERIFICATION FAILED$
9+
--

‎regression/fault-localization/all_properties2/main.c

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#include <assert.h>
2+
3+
void main()
4+
{
5+
int x, c;
6+
if(c) x=0;
7+
else x++;
8+
assert(x==0);
9+
assert(x==0 || c==0);
10+
}

‎regression/fault-localization/all_properties2/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--localize-faults
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
line 7 function main$
7+
^VERIFICATION FAILED$
8+
--

‎regression/fault-localization/stop_on_fail1/main.c

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#include <assert.h>
2+
3+
void main()
4+
{
5+
int x, c;
6+
if(c) x=0;
7+
else x++;
8+
assert(x==0);
9+
assert(x!=0);
10+
}

‎regression/fault-localization/stop_on_fail1/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+
--localize-faults --stop-on-fail
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\]:
7+
line . function main$
8+
^VERIFICATION FAILED$
9+
--

‎regression/run-datastax.sh

Lines changed: 0 additions & 13 deletions
This file was deleted.

0 commit comments

Comments
 (0)