Skip to content

Commit 8103a17

Browse files
author
Daniel Kroening
committed
2 parents 14f0e63 + bbae05d commit 8103a17

Some content is hidden

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

55 files changed

+1255
-330
lines changed

‎regression/ansi-c/Universal_characters1/main.c

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
int identifier_\u0201_;
2+
int \u0201_abc;
3+
4+
#define STATIC_ASSERT(condition) \
5+
int some_array##__LINE__[(condition) ? 1 : -1];
6+
7+
char my_string[]="\u0201";
8+
STATIC_ASSERT(sizeof(my_string)==3);
9+
10+
// also as character literal
11+
STATIC_ASSERT(L'\u0201'==0x0201);
12+
13+
int main()
14+
{
15+
identifier_ȁ_=10;
16+
ȁ_abc=10;
17+
}
18+

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$

‎regression/ansi-c/float_constant1/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,9 @@ STATIC_ASSERT(0x1.0p-95f == 2.524355e-29f);
77
// also with upper case X, P, F
88
STATIC_ASSERT(0X1.0P-95F == 2.524355e-29f);
99

10+
// nothing before the dot
11+
STATIC_ASSERT(0X.0p+1f == 0);
12+
1013
#ifdef __GNUC__
1114
_Complex c;
1215
#endif

‎regression/ansi-c/gcc_builtins1/main.c

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,17 @@
11
#ifdef __GNUC__
22

3-
enum { E1 = __builtin_isinf(1.0) };
4-
enum { E2 = __builtin_isnan(1.0) };
5-
enum { E3 = __builtin_isinf(__builtin_inf()) };
6-
enum { E4 = __builtin_signbit(-1.0) };
7-
enum { E5 = __builtin_classify_type(1) };
8-
enum { E6 = sizeof(int) };
9-
enum { E7 = __alignof__(int) };
10-
enum { E8 = (int)1.0 };
11-
enum { E9 = __builtin_popcount(123) };
3+
enum { E01 = __builtin_isinf(1.0) };
4+
enum { E02 = __builtin_isnan(1.0) };
5+
enum { E03 = __builtin_isinf(__builtin_inf()) };
6+
enum { E04 = __builtin_signbit(-1.0) }; // clang doesn't do this one
7+
enum { E05 = __builtin_classify_type(1) };
8+
enum { E06 = sizeof(int) };
9+
enum { E07 = __alignof__(int) };
10+
enum { E08 = (int)1.0 };
11+
enum { E09 = __builtin_popcount(123) };
12+
enum { E10 = __builtin_bswap16(0xaabb) };
13+
enum { E11 = __builtin_bswap32(0xaabb) };
14+
enum { E12 = __builtin_bswap64(0xaabb) };
1215

1316
#endif
1417

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ main.c
33

44
^EXIT=10$
55
^SIGNAL=0$
6-
^start_thread in atomic section detected$
6+
^file main.c line 12 function spawn: start_thread in atomic section detected$
77
--
88
^warning: ignoring

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,4 +17,6 @@ int main()
1717
else
1818
{
1919
}
20+
21+
return 1;
2022
}

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

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,13 @@ main.c
33
--cover mcdc
44
^EXIT=0$
55
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 14 function main MC/DC independence condition `C && D && !E && A && !B.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 14 function main MC/DC independence condition `C && !D && E && A && !B.*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 14 function main MC/DC independence condition `!C && D && E && A && !B.*: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 14 function main MC/DC independence condition `C && D && E && A && !B.*: SATISFIED$
10+
^\[main.coverage.5\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$
11+
^\[main.coverage.6\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$
612
^\*\* .* of .* covered (100.0%)$
7-
^\*\* Used 6 iterations$
13+
^\*\* Used 10 iterations$
814
--
915
^warning: ignoring

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
int main()
2+
{
3+
4+
__CPROVER_bool A, B, C;
5+
6+
__CPROVER_input("A", A);
7+
__CPROVER_input("B", B);
8+
__CPROVER_input("C", C);
9+
10+
if(A||B||C)
11+
{
12+
}
13+
else
14+
{
15+
}
16+
17+
return 1;
18+
}

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

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--cover mcdc
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A && !B && !C.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!A && B && !C.*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!A && !B && C.*: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && !B && !C.*: SATISFIED$
10+
^\*\* .* of .* covered (100.0%)$
11+
^\*\* Used 6 iterations$
12+
--
13+
^warning: ignoring

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int main()
2+
{
3+
unsigned x, y;
4+
if (!(x>3) && y<5)
5+
;
6+
7+
return 1;
8+
}

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--cover mcdc
4+
^EXIT=0$
5+
^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$
9+
^\*\* .* of .* covered (100.0%)$
10+
^\*\* Used 4 iterations$
11+
--
12+
^warning: ignoring

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
int main()
2+
{
3+
4+
__CPROVER_bool A, B, C, D;
5+
6+
__CPROVER_input("A", A);
7+
__CPROVER_input("B", B);
8+
__CPROVER_input("C", C);
9+
__CPROVER_input("D", D);
10+
11+
if((A && B) || (C && D))
12+
{
13+
}
14+
else
15+
{
16+
}
17+
18+
return 1;
19+
}

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

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--cover mcdc
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 11 function main MC/DC independence condition `A && B && C && !D.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 11 function main MC/DC independence condition `A && !B && C && D.*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 11 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
10+
^\[main.coverage.5\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
11+
^\*\* .* of .* covered (100.0%)$
12+
^\*\* Used 9 iterations$
13+
--
14+
^warning: ignoring

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
int main()
2+
{
3+
__CPROVER_bool A, B, C, D;
4+
5+
__CPROVER_input("A", A);
6+
__CPROVER_input("B", B);
7+
__CPROVER_input("C", C);
8+
__CPROVER_input("D", D);
9+
10+
if((A || B) && (C || D))
11+
{
12+
}
13+
else
14+
{
15+
}
16+
17+
return 1;
18+
}

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

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--cover mcdc
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!C && !D && A && !B.*: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
10+
^\[main.coverage.5\] file main.c line 10 function main MC/DC independence condition `!A && !B && C && !D.*: SATISFIED$
11+
^\*\* .* of .* covered (100.0%)$
12+
^\*\* Used 9 iterations$
13+
--
14+
^warning: ignoring

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int main()
2+
{
3+
unsigned x;
4+
if(x<3)
5+
;
6+
7+
return 1;
8+
}

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--cover mcdc
4+
^EXIT=0$
5+
^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$
8+
^\*\* .* of .* covered (100.0%)$
9+
^\*\* Used 2 iterations$
10+
--
11+
^warning: ignoring

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int main()
2+
{
3+
signed x, y;
4+
5+
y = x*123<0 ? 0 : (x*123>100 ? 100 : x*123 );
6+
7+
return 1;
8+
}

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

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--cover mcdc
4+
^EXIT=0$
5+
^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$
10+
^\*\* .* of .* covered (100.0%)$
11+
^\*\* Used 2 iterations$
12+
--
13+
^warning: ignoring

‎regression/cegis/cegis_danger_benchmark_01_19/run-cbmc-danger-benchmark.sh

Lines changed: 27 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,31 @@
11
#!/bin/bash
2-
#export PATH=${PATH//cbmc-5190/cbmc-trunk-synth}
3-
tool=/users/pkesseli/software/cpp/cbmc/cbmc-trunk-diffblue/regression/cbmc-wrapper.sh
4-
#benchmark_dir=${regression_dir}/cegis-cbmc
5-
result_file=$1.cbmc.log
6-
export out_file=$1.cbmc.out
2+
tool=$1
3+
export out_file=$2.cbmc.out
74
rm ${out_file} 2>/dev/null
85
timeout_time=300
96

10-
start_time=$(date +%s.%N)
11-
timeout --kill-after=10 ${timeout_time} bash ${tool} --no-unwinding-assertions $1
12-
end_time=$(date +%s.%N)
13-
duration=$(echo "${end_time} - ${start_time}" | bc)
14-
grep "VERIFICATION FAILED" ${out_file} >/dev/null
15-
error_found=$?
16-
grep "VERIFICATION SUCCESSFUL" ${out_file} >/dev/null
17-
no_bugs=$?
18-
if [ ${error_found} -eq 0 ]; then
19-
echo -e "${benchmark}\tFALSE\t${duration}" >>"${result_file}"
20-
elif [ ${no_bugs} -eq 0 ]; then
21-
echo -e "${benchmark}\tTRUE\t${duration}" >>"${result_file}"
22-
else
23-
echo -e "${benchmark}\tUNKNOWN\t${duration}" >>"${result_file}"
24-
fi
7+
start_time=$(($(date +%s%N)/1000000))
8+
timeout --kill-after=10 ${timeout_time} bash ${tool} --no-unwinding-assertions $2
9+
if [ $? -eq 124 ]; then
10+
timed_out=0
11+
else
12+
timed_out=1
13+
fi
14+
end_time=$(($(date +%s%N)/1000000))
15+
duration=$(echo "${end_time} - ${start_time}" | bc)
16+
grep "VERIFICATION FAILED" ${out_file} >/dev/null
17+
error_found=$?
18+
grep "VERIFICATION SUCCESSFUL" ${out_file} >/dev/null
19+
no_bugs=$?
20+
if [ ${timed_out} -eq 0 ]; then
21+
echo -e "${benchmark}\tTIMEOUT\t${duration}" >>"${out_file}"
22+
elif [ ${error_found} -eq 0 ]; then
23+
echo -e "${benchmark}\tVER-FALSE\t${duration}" >>"${out_file}"
24+
elif [ ${no_bugs} -eq 0 ]; then
25+
echo -e "${benchmark}\tVER-TRUE\t${duration}" >>"${out_file}"
26+
else
27+
echo -e "${benchmark}\tUNKNOWN\t${duration}" >>"${out_file}"
28+
fi
29+
30+
echo "<full_time> ${duration}</full_time>" >>"${out_file}"
31+
echo "</stats>" >>"${out_file}"

0 commit comments

Comments
 (0)