Skip to content

Commit a290568

Browse files
kroeningkroening
committed
Merge branch 'master' of https://github.com/diffblue/cbmc 
2 parents aec4799 + 587689d commit a290568

File tree

270 files changed

+5217
-918
lines changed

Some content is hidden

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

270 files changed

+5217
-918
lines changed

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ src/util/irep_ids.inc
2323
# regression/test files
2424
*.out
2525
regression/ansi-c/tests.log
26+
regression/symex/tests.log
2627
regression/cbmc-java/tests.log
2728
regression/cbmc/tests.log
2829
src/big-int/test-bigint

‎regression/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
DIRS = ansi-c cbmc cpp
1+
DIRS = ansi-c cbmc cpp goto-instrument
22

33
test:
44
$(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;)

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
2+
enum {
3+
E0 = (int)(4./1.)
4+
};
5+
6+
int main (void) {
7+
return 0;
8+
}
9+

‎regression/ansi-c/enum8/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+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$

‎regression/cbmc-cover/mcdc10/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+
_Bool A, B, C;
4+
5+
__CPROVER_input("cold", A);
6+
__CPROVER_input("raining", B);
7+
__CPROVER_input("windy", C);
8+
9+
if ( A || B || C )
10+
{
11+
/* instructions */
12+
}
13+
else
14+
{
15+
/* instructions */
16+
}
17+
18+
return 1;
19+
}

‎regression/cbmc-cover/mcdc10/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 9 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && !(C != FALSE).*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && !(C != FALSE).*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && C != FALSE.*: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && !(C != FALSE).*: SATISFIED$
10+
^\*\* .* of .* covered (100.0%)$
11+
^\*\* Used 5 iterations$
12+
--
13+
^warning: ignoring

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

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
int main()
2+
{
3+
_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)
11+
{
12+
if (C || D)
13+
{
14+
/* instructions */
15+
}
16+
else
17+
{
18+
/* instructions */
19+
}
20+
}
21+
else
22+
{
23+
/* instructions */
24+
}
25+
26+
return 1;
27+
}

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

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

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

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
int main()
2+
{
3+
_Bool A, B, C, D, E, F;
4+
5+
__CPROVER_input("A", A);
6+
__CPROVER_input("B", B);
7+
__CPROVER_input("C", C);
8+
__CPROVER_input("D", D);
9+
__CPROVER_input("E", D);
10+
__CPROVER_input("F", D);
11+
12+
if (A && B)
13+
{
14+
if (C || D)
15+
{
16+
/* instructions */
17+
}
18+
else
19+
{
20+
/* instructions */
21+
}
22+
}
23+
else
24+
{
25+
if (E || F)
26+
{
27+
/* instructions */
28+
}
29+
else
30+
{
31+
/* instructions */
32+
}
33+
}
34+
35+
return 1;
36+
}

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

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

0 commit comments

Comments
 (0)