Skip to content

Commit 1f2c16b

Browse files
Call CProver methods from SVCOMP's Verifier class
1 parent 1068a99 commit 1f2c16b

File tree

1 file changed

+72
-0
lines changed

1 file changed

+72
-0
lines changed
Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
/*
2+
* Contributed by Peter Schrammel
3+
*
4+
* Licensed under the Apache License, Version 2.0 (the "License");
5+
* you may not use this file except in compliance with the License.
6+
* You may obtain a copy of the License at
7+
*
8+
* http://www.apache.org/licenses/LICENSE-2.0
9+
*
10+
* Unless required by applicable law or agreed to in writing, software
11+
* distributed under the License is distributed on an "AS IS" BASIS,
12+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
* See the License for the specific language governing permissions and
14+
* limitations under the License.
15+
*/
16+
17+
package org.sosy_lab.sv_benchmarks;
18+
19+
import org.cprover.CProver;
20+
21+
public final class Verifier
22+
{
23+
public static void assume(boolean condition)
24+
{
25+
CProver.assume(condition);
26+
}
27+
28+
public static boolean nondetBoolean()
29+
{
30+
return CProver.nondetBoolean();
31+
}
32+
33+
public static byte nondetByte()
34+
{
35+
return CProver.nondetByte();
36+
}
37+
38+
public static char nondetChar()
39+
{
40+
return CProver.nondetChar();
41+
}
42+
43+
public static short nondetShort()
44+
{
45+
return CProver.nondetShort();
46+
}
47+
48+
public static int nondetInt()
49+
{
50+
return CProver.nondetInt();
51+
}
52+
53+
public static long nondetLong()
54+
{
55+
return CProver.nondetLong();
56+
}
57+
58+
public static float nondetFloat()
59+
{
60+
return CProver.nondetFloat();
61+
}
62+
63+
public static double nondetDouble()
64+
{
65+
return CProver.nondetDouble();
66+
}
67+
68+
public static String nondetString()
69+
{
70+
return CProver.nondetWithoutNull("");
71+
}
72+
}

0 commit comments

Comments
 (0)