Skip to content

Commit b9665b0

Browse files
smowtonsmowton
committed
Merge remote-tracking branch 'upstream/master' into test_gen_mocks
2 parents 0af4e71 + 96156fe commit b9665b0

Some content is hidden

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

44 files changed

+736
-255
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-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: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
1-
KNOWNBUG
1+
CORE
22
main.class
33
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+
--

‎src/ansi-c/library/jsa.h

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -800,6 +800,7 @@ __CPROVER_jsa_extern __CPROVER_jsa_word_t __CPROVER_JSA_MAX_PRED_SIZE_RELAY[__CP
800800
__CPROVER_jsa_extern __CPROVER_jsa_word_t __CPROVER_JSA_MAX_QUERY_SIZE_RELAY[__CPROVER_JSA_MAX_QUERY_SIZE];
801801
__CPROVER_jsa_extern __CPROVER_jsa_word_t __CPROVER_JSA_MAX_ITERATORS_RELAY[__CPROVER_JSA_MAX_ITERATORS];
802802
__CPROVER_jsa_extern __CPROVER_jsa_word_t __CPROVER_JSA_MAX_LISTS_RELAY[__CPROVER_JSA_MAX_LISTS];
803+
__CPROVER_jsa_extern __CPROVER_jsa_word_t __CPROVER_JSA_MAX_NODES_PER_LIST_RELAY[__CPROVER_JSA_MAX_NODES_PER_LIST];
803804
//__CPROVER_jsa_extern __CPROVER_jsa_word_t __CPROVER_JSA_HEAP_VARS[__CPROVER_JSA_NUM_PRED_RESULT_OPS];
804805
//__CPROVER_jsa_extern __CPROVER_jsa_word_t __CPROVER_JSA_ORG_HEAP_VARS[__CPROVER_JSA_NUM_PRED_RESULT_OPS];
805806
//__CPROVER_jsa_extern __CPROVER_jsa_word_t __CPROVER_JSA_QUERIED_HEAP_VARS[__CPROVER_JSA_NUM_PRED_RESULT_OPS];
@@ -932,11 +933,15 @@ __CPROVER_jsa_inline void __CPROVER_jsa_stream_op(
932933
__CPROVER_jsa_abstract_heapt * const heap,
933934
const __CPROVER_jsa_list_id_t list,
934935
const __CPROVER_jsa_iterator_id_t it,
935-
const __CPROVER_jsa_list_id_t copy,
936+
const __CPROVER_jsa_list_id_t source,
936937
const __CPROVER_jsa_pred_id_t pred_id,
937938
const __CPROVER_jsa__internal_index_t id)
938939
{
939-
__CPROVER_jsa_node_id_t node=__CPROVER_jsa__internal_get_head_node(heap, list);
940+
__CPROVER_jsa_node_id_t node;
941+
if (__CPROVER_jsa_null == source)
942+
node = __CPROVER_jsa__internal_get_head_node(heap, list);
943+
else
944+
node = __CPROVER_jsa__internal_get_head_node(heap, source);
940945
const __CPROVER_jsa_node_id_t end=heap->iterators[it].node_id;
941946
for (__CPROVER_jsa__internal_index_t i=0; i < __CPROVER_JSA_MAX_NODES_PER_LIST; ++i)
942947
{
@@ -957,10 +962,10 @@ __CPROVER_jsa_inline void __CPROVER_jsa_stream_op(
957962
break;
958963
case COPY_IF:
959964
if (pred_result != 0)
960-
__CPROVER_jsa_add(heap, copy, value);
965+
__CPROVER_jsa_add(heap, list, value);
961966
break;
962967
case MAP:
963-
__CPROVER_jsa_add(heap, copy, pred_result);
968+
__CPROVER_jsa_add(heap, list, pred_result);
964969
break;
965970
case MAP_IN_PLACE:
966971
heap->concrete_nodes[node].value=pred_result;

‎src/ansi-c/literals/convert_string_literal.cpp

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ void convert_one_string_literal(
3434
std::basic_string<unsigned int> &value)
3535
{
3636
assert(src.size()>=2);
37-
37+
3838
if(src[0]=='u' && src[1]=='8')
3939
{
4040
assert(src[src.size()-1]=='"');
@@ -63,6 +63,14 @@ void convert_one_string_literal(
6363
assert(src[src.size()-1]=='"');
6464

6565
unescape_wide_string(std::string(src, 1, src.size()-2), value);
66+
67+
// turn into utf-8
68+
std::string utf8_value=utf32_to_utf8(value);
69+
70+
// pad into wide string
71+
value.resize(utf8_value.size());
72+
for(unsigned i=0; i<utf8_value.size(); i++)
73+
value[i]=utf8_value[i];
6674
}
6775
}
6876

‎src/ansi-c/scanner.l

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -150,7 +150,8 @@ digit [0-9]
150150
bindigit [01]
151151
octdigit [0-7]
152152
hexdigit [0-9a-fA-F]
153-
identifier (({letter}|"_"|"$")({letter}|{digit}|"_"|"$")*)
153+
utf8letter [\x80-\xff]
154+
identifier (({letter}|"_"|"$"|{utf8letter})({letter}|{digit}|"_"|"$"|{utf8letter})*)
154155
integer {digit}+
155156
binary {bindigit}+
156157
msiw_suffix ([iI]("8"|"16"|"32"|"64"|"128"))

‎src/cegis/Makefile

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -88,19 +88,20 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
8888
../cbmc/symex_bmc$(OBJEXT) ../cbmc/xml_interface$(OBJEXT) ../cbmc/bmc_cover$(OBJEXT) \
8989
../cbmc/bv_cbmc$(OBJEXT) ../cbmc/counterexample_beautification$(OBJEXT) \
9090
../cbmc/cbmc_languages$(OBJEXT) ../cbmc/show_vcc$(OBJEXT) \
91-
../cbmc/cbmc_dimacs$(OBJEXT) ../cbmc/all_properties$(OBJEXT)
91+
../cbmc/cbmc_dimacs$(OBJEXT) ../cbmc/all_properties$(OBJEXT) \
92+
../cbmc/fault_localization$(OBJEXT)
9293

9394
INCLUDES= -I ..
9495

95-
ifeq ($(filter-out Unix MinGW Cygwin OSX OSX_Universal FreeBSD,$(BUILD_ENV_)),)
96+
include ../config.inc
97+
include ../common
98+
99+
ifeq ($(filter-out Unix MinGW Cygwin OSX OSX_Universal,$(BUILD_ENV_)),)
96100
DLFCN_LINKFLAGS = -ldl
97101
endif
98102

99103
LIBS = $(DLFCN_LINKFLAGS)
100104

101-
include ../config.inc
102-
include ../common
103-
104105
CLEANFILES = cegis$(EXEEXT)
105106

106107
all: cegis$(EXEEXT)

0 commit comments

Comments
 (0)