Skip to content

Commit 2156227

Browse files
hbgithbgit
committed
Merge branch 'svcomp2018' into nooverflow
Signed-off-by: Herbert Rocha <herberthb12@gmail.com>
2 parents ad55119 + e221d08 commit 2156227

File tree

8 files changed

+84
-43
lines changed

8 files changed

+84
-43
lines changed

‎README.md‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -35,8 +35,8 @@ In order to install Map2Check on your PC, you should download and save the map2c
3535
After that, you should type the following command:
3636
</p>
3737

38-
> $ unzip v7.zip
39-
> $ cd Map2Check-7/release
38+
> $ unzip map2check_v7.1_svcomp.zip
39+
> $ cd Map2Check-map2check_v7.1_svcomp
4040
4141
<b>Testing tool</b>
4242

@@ -45,11 +45,11 @@ Map2Check can be invoked through a standard command-line interface. Map2Check sh
4545
in the installation directory as follows:
4646
</p>
4747

48-
> $ ./map2check sample/sv-comp/960521-1_false-valid-free.c
48+
> $ ./map2check sample/svcomp_960521-1_false-valid-free.c
4949
5050
For help and others options:
5151

52-
> $ ./map2check -h
52+
> $ ./map2check --help
5353
5454
===========================
5555

@@ -68,7 +68,7 @@ FALSE(p), with p in {valid-free, valid-deref, valid-memtrack}, means that the (p
6868
property p is violated.
6969
For each verification result the witness file (called <b>witness.graphml</b>) is generated Map2Check root-path folder.
7070
There is timeout of 895 seconds set by this script, using "timeout" tool that is part of coreutils
71-
on debian and fedora. If these constraints are violated, it should be treated as UNKNOWN result.
71+
on debian. If these constraints are violated, it should be treated as UNKNOWN result.
7272
</p>
7373

7474
===========================

‎lib/Map2CheckFunctions.bc‎

8 Bytes
Binary file not shown.

‎map2check‎

16.4 KB
Binary file not shown.

‎moduleBenchExec/map2check.py‎

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -36,10 +36,11 @@ class Tool(benchexec.tools.template.BaseTool):
3636
]
3737

3838
REQUIRED_PATHS_7_1 = [
39-
"__init__.py",
4039
"map2check",
4140
"map2check-wrapper.py",
42-
"modules"
41+
"bin",
42+
"include",
43+
"lib"
4344
]
4445

4546
def executable(self):
@@ -51,14 +52,15 @@ def executable(self):
5152

5253

5354
def program_files(self, executable):
54-
executableDir = os.path.dirname(executable)
55-
55+
"""
56+
Determine the file paths to be adopted
57+
"""
5658
if self._get_version() == 6:
57-
paths = REQUIRED_PATHS_6
59+
paths = self.REQUIRED_PATHS_6
5860
elif self._get_version() > 6:
59-
paths = REQUIRED_PATHS_7_1
61+
paths = self.REQUIRED_PATHS_7_1
6062

61-
return [executableDir] + paths
63+
return paths
6264

6365
def _get_version(self):
6466
"""
@@ -136,4 +138,3 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
136138
status = 'ERROR'
137139

138140
return status
139-

‎moduleBenchExec/map2check.xml‎

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
<?xml version="1.0"?>
2+
<!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.4//EN" "http://www.sosy-lab.org/benchexec/benchmark-1.4.dtd">
3+
<benchmark tool="map2check" timelimit="900 s" memlimit="15 GB" cpuCores="8">
4+
5+
<require cpuModel="Intel Xeon E3-1230 v5 @ 3.40 GHz" cpuCores="8"/>
6+
7+
<resultfiles>**.graphml</resultfiles>
8+
9+
<rundefinition name="sv-comp18"></rundefinition>
10+
11+
<tasks name="ReachSafety-Arrays">
12+
<includesfile>../sv-benchmarks/c/ReachSafety-Arrays.set</includesfile>
13+
<propertyfile>../sv-benchmarks/c/ReachSafety.prp</propertyfile>
14+
</tasks>
15+
<tasks name="ReachSafety-BitVectors">
16+
<includesfile>../sv-benchmarks/c/ReachSafety-BitVectors.set</includesfile>
17+
<propertyfile>../sv-benchmarks/c/ReachSafety.prp</propertyfile>
18+
</tasks>
19+
<tasks name="ReachSafety-Heap">
20+
<includesfile>../sv-benchmarks/c/ReachSafety-Heap.set</includesfile>
21+
<propertyfile>../sv-benchmarks/c/ReachSafety.prp</propertyfile>
22+
</tasks>
23+
<tasks name="ReachSafety-Loops">
24+
<includesfile>../sv-benchmarks/c/ReachSafety-Loops.set</includesfile>
25+
<propertyfile>../sv-benchmarks/c/ReachSafety.prp</propertyfile>
26+
</tasks>
27+
<tasks name="ReachSafety-Recursive">
28+
<includesfile>../sv-benchmarks/c/ReachSafety-Recursive.set</includesfile>
29+
<propertyfile>../sv-benchmarks/c/ReachSafety.prp</propertyfile>
30+
</tasks>
31+
32+
33+
<tasks name="MemSafety-Arrays">
34+
<includesfile>../sv-benchmarks/c/MemSafety-Arrays.set</includesfile>
35+
<propertyfile>../sv-benchmarks/c/MemSafety.prp</propertyfile>
36+
</tasks>
37+
<tasks name="MemSafety-Heap">
38+
<includesfile>../sv-benchmarks/c/MemSafety-Heap.set</includesfile>
39+
<propertyfile>../sv-benchmarks/c/MemSafety.prp</propertyfile>
40+
</tasks>
41+
<tasks name="MemSafety-LinkedLists">
42+
<includesfile>../sv-benchmarks/c/MemSafety-LinkedLists.set</includesfile>
43+
<propertyfile>../sv-benchmarks/c/MemSafety.prp</propertyfile>
44+
</tasks>
45+
<tasks name="MemSafety-Other">
46+
<includesfile>../sv-benchmarks/c/MemSafety-Other.set</includesfile>
47+
<propertyfile>../sv-benchmarks/c/MemSafety.prp</propertyfile>
48+
</tasks>
49+
50+
51+
<tasks name="NoOverflows-BitVectors">
52+
<includesfile>../sv-benchmarks/c/NoOverflows-BitVectors.set</includesfile>
53+
<propertyfile>../sv-benchmarks/c/NoOverflows.prp</propertyfile>
54+
</tasks>
55+
<tasks name="NoOverflows-Other">
56+
<includesfile>../sv-benchmarks/c/NoOverflows-Other.set</includesfile>
57+
<propertyfile>../sv-benchmarks/c/NoOverflows.prp</propertyfile>
58+
</tasks>
59+
60+
</benchmark>

‎sample/Muller_Kahan_true-unreach-call.c‎

Lines changed: 0 additions & 27 deletions
This file was deleted.

‎sample/example-1_TRUE.i‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ extern int __VERIFIER_nondet_int(void);
33

44
int main() {
55
unsigned int x = 1;
6-
while(x > 10) {
6+
while(x > 1) {
77
x = x + 2;
88
}
9-
if (x >= 5) __VERIFIER_error();
9+
if (x > 1) __VERIFIER_error();
1010
return 0;
1111
}

‎sample/svcomp_960521-1_false-valid-free.c‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -626,10 +626,17 @@ void foo ()
626626
for (i = 0; i < 128 - 1; i++)
627627
b[i] = -1;
628628
}
629+
630+
void call(){
631+
int a;
632+
a = a+1;
633+
}
634+
629635
int main ()
630636
{
631-
n = 128;
637+
n = 128;
632638
a = malloc (n * sizeof(*a));
639+
call();
633640
b = malloc (n * sizeof(*b));
634641
*b++ = 0;
635642
foo ();

0 commit comments

Comments
 (0)