Skip to content

Commit 0266e23

Browse files
tautschnigtautschnig
authored
Merge pull request #66 from FrNecas/instrument
Replace reach_error (or equivalent) with assert(0)
2 parents 09a869e + 0ac3d0d commit 0266e23

File tree

6 files changed

+42
-16
lines changed

6 files changed

+42
-16
lines changed

‎2ls.inc

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,11 @@ run()
1111
gmon_suffix=$GMON_OUT_PREFIX
1212
export GMON_OUT_PREFIX="goto-cc_$gmon_suffix"
1313
./goto-cc -m$BIT_WIDTH --function $ENTRY "${BM[@]}" -o $LOG.bin
14+
if [ -n "$FAIL_FUNCTION" ]; then
15+
./goto-instrument $LOG.bin $LOG.bin --remove-function-body "$FAIL_FUNCTION" \
16+
--generate-function-body "$FAIL_FUNCTION" \
17+
--generate-function-body-options assert-false
18+
fi
1419

1520
export GMON_OUT_PREFIX="2ls_$gmon_suffix"
1621
# add property-specific options

‎Makefile

Lines changed: 12 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ jbmc: jbmc.zip
1919
cat $*.inc tool-wrapper.inc >> $@
2020
chmod 755 $@
2121

22-
cbmc-path.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC)/src/goto-cc/goto-cc sv-comp-readme.sh
22+
cbmc-path.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC)/src/goto-cc/goto-cc $(CBMC)/src/goto-instrument/goto-instrument sv-comp-readme.sh
2323
mkdir -p $(basename $@)
2424
$(MAKE) cbmc-wrapper
2525
mv cbmc-wrapper $(basename $@)/cbmc
@@ -30,12 +30,14 @@ cbmc-path.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $
3030
strip $(basename $@)/cbmc-binary
3131
cp -L $(CBMC)/src/goto-cc/goto-cc $(basename $@)/
3232
strip $(basename $@)/goto-cc
33+
cp -L $(CBMC)/src/goto-instrument/goto-instrument $(basename $@)/
34+
strip $(basename $@)/goto-instrument
3335
chmod a+rX $(basename $@)/*
3436
zip -r $@ $(basename $@)
35-
cd $(basename $@) && rm cbmc cbmc-binary goto-cc LICENSE README
37+
cd $(basename $@) && rm cbmc cbmc-binary goto-cc goto-instrument LICENSE README
3638
rmdir $(basename $@)
3739

38-
cbmc.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC)/src/goto-cc/goto-cc sv-comp-readme.sh
40+
cbmc.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC)/src/goto-cc/goto-cc $(CBMC)/src/goto-instrument/goto-instrument sv-comp-readme.sh
3941
mkdir -p $(basename $@)
4042
$(MAKE) cbmc-wrapper
4143
mv cbmc-wrapper $(basename $@)/cbmc
@@ -45,12 +47,14 @@ cbmc.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC
4547
strip $(basename $@)/cbmc-binary
4648
cp -L $(CBMC)/src/goto-cc/goto-cc $(basename $@)/
4749
strip $(basename $@)/goto-cc
50+
cp -L $(CBMC)/src/goto-instrument/goto-instrument $(basename $@)/
51+
strip $(basename $@)/goto-instrument
4852
chmod a+rX $(basename $@)/*
4953
zip -r $@ $(basename $@)
50-
cd $(basename $@) && rm cbmc cbmc-binary goto-cc LICENSE README
54+
cd $(basename $@) && rm cbmc cbmc-binary goto-cc goto-instrument LICENSE README
5155
rmdir $(basename $@)
5256

53-
2ls.zip: 2ls.inc tool-wrapper.inc $(2LS)/LICENSE $(2LS)/src/2ls/2ls $(2LS)/lib/cbmc/src/goto-cc/goto-cc sv-comp-readme.sh
57+
2ls.zip: 2ls.inc tool-wrapper.inc $(2LS)/LICENSE $(2LS)/src/2ls/2ls $(2LS)/lib/cbmc/src/goto-cc/goto-cc $(2LS)/lib/cbmc/src/goto-instrument/goto-instrument sv-comp-readme.sh
5458
mkdir -p $(basename $@)
5559
$(MAKE) 2ls-wrapper
5660
mv 2ls-wrapper $(basename $@)/2ls
@@ -60,9 +64,11 @@ cbmc.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC
6064
strip $(basename $@)/2ls-binary
6165
cp -L $(2LS)/lib/cbmc/src/goto-cc/goto-cc $(basename $@)/
6266
strip $(basename $@)/goto-cc
67+
cp -L $(2LS)/lib/cbmc/src/goto-instrument/goto-instrument $(basename $@)/
68+
strip $(basename $@)/goto-instrument
6369
chmod a+rX $(basename $@)/*
6470
zip -r $@ $(basename $@)
65-
cd $(basename $@) && rm 2ls 2ls-binary goto-cc LICENSE README
71+
cd $(basename $@) && rm 2ls 2ls-binary goto-cc goto-instrument LICENSE README
6672
rmdir $(basename $@)
6773

6874
jbmc.zip: jbmc.inc tool-wrapper.inc $(JBMC)/LICENSE $(JBMC)/jbmc/src/jbmc/jbmc $(JBMC)/jbmc/lib/java-models-library/target/core-models.jar sv-comp-readme.sh

‎README.cbmc-path.txt

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,16 +6,20 @@ This archive contains the following files:
66
- goto-cc: this C compiler transforms input files into so-called
77
`goto-binaries,' which are encoded in CBMC's intermediate representation.
88

9+
- goto-instrument: performs required preliminary transformations on the
10+
'goto-binary'.
11+
912
- cbmc-binary: this is the actual verification tool. It takes a goto-binary
1013
as input and checks the properties specified by command-line flags.
1114

12-
- cbmc: this wrapper script invokes cbmc-binary and goto-cc, parsing the
13-
property file to pass the correct flags to cbmc-binary and returning the
14-
correct return codes for SV-COMP.
15+
- cbmc: this wrapper script invokes cbmc-binary, goto-cc and goto-instrument,
16+
parsing the property file to pass the correct flags to cbmc-binary and
17+
returning the correct return codes for SV-COMP.
1518

16-
goto-cc and cbmc-binary were compiled on Debian 9 (stretch); the binaries
17-
should be self-hosting on similar operating systems. The upstream URL, if
18-
you wish to compile it yourself, is https://github.com/diffblue/cbmc
19+
goto-cc, goto-instrument and cbmc-binary were compiled on Debian 9 (stretch);
20+
the binaries should be self-hosting on similar operating systems.
21+
The upstream URL, if you wish to compile it yourself, is
22+
https://github.com/diffblue/cbmc
1923

2024
To run CBMC Path manually, you need to invoke the tool as
2125

‎cbmc.inc

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,11 @@ run()
1515
gmon_suffix=$GMON_OUT_PREFIX
1616
export GMON_OUT_PREFIX="goto-cc_$gmon_suffix"
1717
./goto-cc --object-bits $OBJ_BITS -m$BIT_WIDTH --function $ENTRY "${BM[@]}" -o $LOG.bin
18+
if [ -n "$FAIL_FUNCTION" ]; then
19+
./goto-instrument $LOG.bin $LOG.bin --remove-function-body "$FAIL_FUNCTION" \
20+
--generate-function-body "$FAIL_FUNCTION" \
21+
--generate-function-body-options assert-false
22+
fi
1823

1924
export GMON_OUT_PREFIX="cbmc_$gmon_suffix"
2025
timeout 875 bash -c ' \

‎sv-comp-readme.sh

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -36,13 +36,16 @@ then
3636
- goto-cc: this C compiler transforms input files into so-called
3737
"goto-binaries," which are encoded in CBMC's intermediate representation.
3838
39+
- goto-instrument: performs required preliminary transformations on the
40+
"goto-binary".
41+
3942
- $TOOL-binary: this is the actual verification tool. It takes a goto-binary or
4043
source code as input and checks the properties specified by command-line
4144
flags.
4245
43-
- $TOOL: this wrapper script invokes $TOOL-binary and goto-cc, parsing the
44-
property file to pass the correct flags to $TOOL-binary and returning the
45-
correct return codes for SV-COMP.
46+
- $TOOL: this wrapper script invokes $TOOL-binary, goto-cc and goto-instrument,
47+
parsing the property file to pass the correct flags to $TOOL-binary and
48+
returning the correct return codes for SV-COMP.
4649
EOF
4750
else
4851
cat <<EOF

‎tool-wrapper.inc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,10 @@ parse_property_file()
2020
if(/^CHECK\(init\((\S+)\(\)\),LTL\((\S+)\)\)$/) {
2121
print "ENTRY=$1\n";
2222
print "PROP=\"label\"\nLABEL=\"$1\"\n" if($2 =~ /^G!label\((\S+)\)$/);
23-
print "PROP=\"unreach_call\"\n" if($2 =~ /^G!call\(reach_error\(\)\)$/);
23+
if($2 =~ /^G!call\((?<fn>\S+)\(\)\)$/) {
24+
print "PROP=\"unreach_call\"\n";
25+
print "FAIL_FUNCTION=\"$+{fn}\"\n";
26+
}
2427
print "PROP=\"unreach_call\"\n" if($2 =~ /^Gassert$/);
2528
print "PROP=\"memsafety\"\n" if($2 =~ /^Gvalid-(free|deref|memtrack)$/);
2629
print "PROP=\"memcleanup\"\n" if($2 =~ /^Gvalid-memcleanup$/);

0 commit comments

Comments
 (0)