Skip to content

Commit f458a87

Browse files
Add test checking if trace bug in field sensitivity was fixed
The test in this commit checks for a bug in which the initial nondet assignment to struct fields was missing from --trace (always showing these struct fields as being initialised to 0).
1 parent 7c6370a commit f458a87

File tree

2 files changed

+27
-0
lines changed
  • regression/cbmc/field-sensitivity-trace-wrong-counterexample-1

2 files changed

+27
-0
lines changed
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
struct SomeStruct
2+
{
3+
int x;
4+
};
5+
6+
int main(void)
7+
{
8+
struct SomeStruct x;
9+
// this should cause
10+
// visible initialization of
11+
// x to value other than 0
12+
// if assertion fails
13+
assert(x.x == 0);
14+
}
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
KNOWNBUG
2+
test.c
3+
--trace
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
x=\{ \.x=-?[123456789]\d* \}
8+
--
9+
^warning: ignoring
10+
--
11+
This tests for the counterexample shown in the trace having sensible values.
12+
In this case, we are asserting that x.x == 0, so x.x should have a value other
13+
than 0 if the assertion fails.

0 commit comments

Comments
 (0)