Skip to content

Commit a673e5d

Browse files
author
Lukasz A.J. Wrona
committed
Add test verifying that the cproverNondetInitialize method is always loaded
Test is disabled because of test-runner problems described in the following issue: #2267
1 parent 971a34b commit a673e5d

File tree

6 files changed

+34
-0
lines changed

6 files changed

+34
-0
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
import org.cprover.CProver;
2+
3+
class ObjectWithNondetInitialize {
4+
private int value_;
5+
public void cproverNondetInitialize() {
6+
CProver.assume(value_ == 13);
7+
}
8+
public int value() {
9+
return value_;
10+
}
11+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
import org.cprover.CProver;
2+
3+
public class Opaque {
4+
public ObjectWithNondetInitialize get() {
5+
return new ObjectWithNondetInitialize();
6+
}
7+
}
Binary file not shown.
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
public class Test {
2+
public int test() {
3+
return (new Opaque()).get().value();
4+
}
5+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
KNOWNBUG
2+
Test.class
3+
--function Test.test --show-goto-functions --lazy-methods
4+
EXIT=0
5+
SIGNAL=0
6+
ObjectWithNondetInitialize\.cproverNondetInitialize\(\)
7+
--
8+
--
9+
Check if cproverNondetInitialize method is loaded in an object
10+
returned from an opaque method
11+
https://github.com/diffblue/cbmc/issues/2273

0 commit comments

Comments
 (0)