Skip to content

Commit e54c0e9

Browse files
author
Thomas Kiley
authored
Merge pull request diffblue#338 from thk123/bug/function-flag-on-goto-program
Cause a regeneration of the _start method if a --function is provided
2 parents 63c9a1e + 22f06fd commit e54c0e9

Some content is hidden

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

45 files changed

+656
-35
lines changed

‎appveyor.yml

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,21 @@ test_script:
6161
- cmd: |
6262
cd regression
6363
64+
sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-cbmc/chain.sh || true
65+
sed -i "11s/.*/$GC $NAME.c/" goto-cc-cbmc/chain.sh || true
66+
sed -i "12i mv $NAME.exe $NAME.gb" goto-cc-cbmc/chain.sh || true
67+
cat goto-cc-cbmc/chain.sh || true
68+
69+
sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-goto-analyzer/chain.sh || true
70+
sed -i "11s/.*/$gc $name.c/" goto-cc-goto-analyzer/chain.sh || true
71+
sed -i "12i mv $name.exe $name.gb" goto-cc-goto-analyzer/chain.sh || true
72+
cat goto-cc-goto-analyzer/chain.sh || true
73+
74+
sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-symex/chain.sh || true
75+
sed -i "11s/.*/$gc $name.c/" goto-cc-symex/chain.sh || true
76+
sed -i "12i mv $name.exe $name.gb" goto-cc-symex/chain.sh || true
77+
cat goto-cc-symex/chain.sh || true
78+
6479
rem HACK disable failing tests
6580
rmdir /s /q ansi-c\arch_flags_mcpu_bad
6681
rmdir /s /q ansi-c\arch_flags_mcpu_good

‎regression/Makefile

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,9 @@ DIRS = ansi-c \
55
cbmc-java-inheritance \
66
cpp \
77
goto-analyzer \
8+
goto-cc-cbmc \
9+
goto-cc-goto-analyzer \
10+
goto-cc-goto-symex \
811
goto-diff \
912
goto-gcc \
1013
goto-instrument \

‎regression/cbmc/pointer-function-parameters-2/test.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,9 @@ main.c
44
^\*\* 7 of 7 covered \(100.0%\)$
55
^\*\* Used 4 iterations$
66
^Test suite:$
7-
^a=\(\(signed int \*\*\)NULL\), tmp\$1=[^,]*, tmp\$2=[^,]*$
8-
^a=&tmp\$1!0, tmp\$1=\(\(signed int \*\)NULL\), tmp\$2=[^,]*$
9-
^a=&tmp\$1!0, tmp\$1=&tmp\$2!0, tmp\$2=([012356789][0-9]*|4[0-9]+)$
10-
^a=&tmp\$1!0, tmp\$1=&tmp\$2!0, tmp\$2=4$
7+
^a=\(\(signed int \*\*\)NULL\), tmp\$\d+=[^,]*, tmp\$\d+=[^,]*$
8+
^a=&tmp\$\d+!0, tmp\$\d+=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
9+
^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=([012356789][0-9]*|4[0-9]+)$
10+
^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=4$
1111
--
1212
^warning: ignoring

‎regression/cbmc/pointer-function-parameters/test.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ main.c
44
^\*\* 5 of 5 covered \(100\.0%\)$
55
^\*\* Used 3 iterations$
66
^Test suite:$
7-
^a=\(\(signed int \*\)NULL\), tmp\$1=[^,]*$
8-
^a=&tmp\$1!0, tmp\$1=4$
9-
^a=&tmp\$1!0, tmp\$1=([012356789][0-9]*|4[0-9]+)$
7+
^a=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
8+
^a=&tmp\$\d+!0, tmp\$\d+=4$
9+
^a=&tmp\$\d+!0, tmp\$\d+=([012356789][0-9]*|4[0-9]+)$
1010
--
1111
^warning: ignoring

‎regression/goto-analyzer/regenerate-entry-function/main.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#include <assert.h>
2+
3+
int fun(int x)
4+
{
5+
int i;
6+
if(i>=20)
7+
assert(i>=10);
8+
}
9+
10+
int main(int argc, char** argv)
11+
{
12+
int i;
13+
14+
if(i>=5)
15+
assert(i>=10);
16+
}

‎regression/goto-analyzer/regenerate-entry-function/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+
--function fun --show-goto-functions
4+
^\s*fun\(x\);$
5+
^EXIT=6$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring

‎regression/goto-cc-cbmc/Makefile

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
default: tests.log
2+
3+
test:
4+
@if ! ../test.pl -c ../chain.sh ; then \
5+
../failed-tests-printer.pl ; \
6+
exit 1; \
7+
fi
8+
9+
tests.log:
10+
@if ! ../test.pl -c ../chain.sh ; 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;
21+
22+
clean:
23+
@for dir in *; do \
24+
$(RM) tests.log; \
25+
if [ -d "$$dir" ]; then \
26+
cd "$$dir"; \
27+
$(RM) *.out *.gb; \
28+
cd ..; \
29+
fi \
30+
done

‎regression/goto-cc-cbmc/chain.sh

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#!/bin/bash
2+
3+
SRC=../../../src
4+
5+
GC=$SRC/goto-cc/goto-cc
6+
CBMC=$SRC/cbmc/cbmc
7+
8+
OPTS=$1
9+
NAME=${2%.c}
10+
11+
$GC $NAME.c -o $NAME.gb
12+
$CBMC $NAME.gb $OPTS

‎regression/goto-cc-cbmc/regenerate-entry-function/main.c

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
int fun(int x)
2+
{
3+
if(x > 0)
4+
{
5+
return x * x;
6+
}
7+
else
8+
{
9+
return x;
10+
}
11+
}
12+
13+
int main(int argc, char** argv)
14+
{
15+
if(argc>4)
16+
{
17+
return 0;
18+
}
19+
else
20+
{
21+
return 1;
22+
}
23+
}

‎regression/goto-cc-cbmc/regenerate-entry-function/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+
"--function fun --cover branch"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^x=
7+
--
8+
^warning: ignoring

‎regression/goto-cc-goto-analyzer/Makefile

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
2+
default: tests.log
3+
4+
test:
5+
@if ! ../test.pl -c ../chain.sh ; then \
6+
../failed-tests-printer.pl ; \
7+
exit 1; \
8+
fi
9+
10+
tests.log:
11+
pwd
12+
@if ! ../test.pl -c ../chain.sh ; then \
13+
../failed-tests-printer.pl ; \
14+
exit 1; \
15+
fi
16+
17+
show:
18+
@for dir in *; do \
19+
if [ -d "$$dir" ]; then \
20+
vim -o "$$dir/*.c" "$$dir/*.out"; \
21+
fi; \
22+
done;
23+
24+
clean:
25+
@for dir in *; do \
26+
rm -f tests.log; \
27+
if [ -d "$$dir" ]; then \
28+
cd "$$dir"; \
29+
rm -f *.out *.gb; \
30+
cd ..; \
31+
fi \
32+
done

‎regression/goto-cc-goto-analyzer/chain.sh

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#!/bin/bash
2+
3+
src=../../../src
4+
5+
gc=$src/goto-cc/goto-cc
6+
goto_analyzer=$src/goto-analyzer/goto-analyzer
7+
8+
options=$1
9+
name=${2%.c}
10+
11+
$gc $name.c -o $name.gb
12+
$goto_analyzer $name.gb $options

‎regression/goto-cc-goto-analyzer/regenerate-entry-function/main.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#include <assert.h>
2+
3+
int fun(int x)
4+
{
5+
int i;
6+
if(i>=20)
7+
assert(i>=10);
8+
}
9+
10+
int main(int argc, char** argv)
11+
{
12+
int i;
13+
14+
if(i>=5)
15+
assert(i>=10);
16+
}

‎regression/goto-cc-goto-analyzer/regenerate-entry-function/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+
"--function fun --show-goto-functions"
4+
^\s*fun\(x\);$
5+
^EXIT=6$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring

‎regression/goto-cc-symex/Makefile

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
2+
default: tests.log
3+
4+
test:
5+
@if ! ../test.pl -c ../chain.sh ; then \
6+
../failed-tests-printer.pl ; \
7+
exit 1; \
8+
fi
9+
10+
tests.log:
11+
pwd
12+
@if ! ../test.pl -c ../chain.sh ; then \
13+
../failed-tests-printer.pl ; \
14+
exit 1; \
15+
fi
16+
17+
show:
18+
@for dir in *; do \
19+
if [ -d "$$dir" ]; then \
20+
vim -o "$$dir/*.c" "$$dir/*.out"; \
21+
fi; \
22+
done;
23+
24+
clean:
25+
@for dir in *; do \
26+
rm -f tests.log; \
27+
if [ -d "$$dir" ]; then \
28+
cd "$$dir"; \
29+
rm -f *.out *.gb; \
30+
cd ..; \
31+
fi \
32+
done

‎regression/goto-cc-symex/chain.sh

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#!/bin/bash
2+
3+
src=../../../src
4+
5+
gc=$src/goto-cc/goto-cc
6+
symex=$src/symex/symex
7+
8+
options=$1
9+
name=${2%.c}
10+
11+
$gc $name.c -o $name.gb
12+
$symex $name.gb $options

‎regression/goto-cc-symex/regenerate-entry-function/main.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#include <assert.h>
2+
3+
int fun(int x)
4+
{
5+
int i;
6+
if(i>=20)
7+
assert(i>=10);
8+
}
9+
10+
int main(int argc, char** argv)
11+
{
12+
int i;
13+
14+
if(i>=5)
15+
assert(i>=10);
16+
}

‎regression/goto-cc-symex/regenerate-entry-function/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+
"--function fun --show-goto-functions"
4+
^\s*return.=fun\(x\);$
5+
^EXIT=6$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring

‎regression/symex/regenerate-entry-function/main.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#include <assert.h>
2+
3+
int fun(int x)
4+
{
5+
int i;
6+
if(i>=20)
7+
assert(i>=10);
8+
}
9+
10+
int main(int argc, char** argv)
11+
{
12+
int i;
13+
14+
if(i>=5)
15+
assert(i>=10);
16+
}

‎regression/symex/regenerate-entry-function/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+
--function fun --show-goto-functions
4+
fun\(x\);$
5+
^EXIT=6$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring

‎regression/symex/show-trace1/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--trace
44
^EXIT=10$
@@ -9,3 +9,5 @@ main.c
99
^ k=6 .*$
1010
--
1111
^warning: ignoring
12+
--
13+
diffblue/cbmc#1361

0 commit comments

Comments
 (0)