Add a test case for per-history verification
This shows that call-stack sensitivity (unsurprisingly) can significantly improve results -- but only with the previous patch.
This commit is contained in:
parent
345d7eb5c3
commit
fddd098711
|
@ -0,0 +1,54 @@
|
|||
#include <assert.h>
|
||||
|
||||
void f00(int x, int y)
|
||||
{
|
||||
if(x < 0)
|
||||
{
|
||||
// Unreachable in all traces if they are considered individually
|
||||
assert(x < 0);
|
||||
assert(1);
|
||||
assert(0);
|
||||
}
|
||||
|
||||
assert(x >= 0); // True in all traces
|
||||
assert(x < 0); // False in all traces
|
||||
assert(x < 2); // Split; true in some, false in others
|
||||
|
||||
assert((x <= 0) ? 1 : y); // True in some, unknown in others
|
||||
assert((x <= 1) ? 0 : y); // False in some, unknown in others
|
||||
assert((x <= 2) ? ((x <= 3) ? 1 : 0) : y); // A mix of all three
|
||||
|
||||
if(x < 5)
|
||||
{
|
||||
// Not reachable in all traces
|
||||
assert((x <= 0) ? 1 : y); // True in some, unknown in others
|
||||
assert((x <= 1) ? 0 : y); // False in some, unknown in others
|
||||
assert((x <= 2) ? ((x <= 3) ? 1 : 0) : y); // A mix of all three
|
||||
}
|
||||
|
||||
if(x < 3)
|
||||
{
|
||||
// Not reachable in all traces
|
||||
assert((x <= 0) ? 1 : y); // True in some, unknown in others
|
||||
assert((x <= 1) ? 0 : y); // False in some, unknown in others
|
||||
assert((x <= 2) ? ((x <= 3) ? 1 : 0) : y); // A mix of all three
|
||||
}
|
||||
}
|
||||
|
||||
int nondet_int();
|
||||
|
||||
int main(int argc, char **argv)
|
||||
{
|
||||
int y = nondet_int();
|
||||
|
||||
// Because the history is context sensitive these should be analysed independently
|
||||
// Just showing the domain will merge them giving top for everything interesting
|
||||
f00(0, y);
|
||||
f00(1, y);
|
||||
f00(2, y);
|
||||
f00(3, y);
|
||||
f00(4, y);
|
||||
f00(5, y);
|
||||
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,25 @@
|
|||
CORE
|
||||
main.c
|
||||
--verify --recursive-interprocedural --call-stack 0 --constants --one-domain-per-history
|
||||
^\[f00.assertion.1\] .* assertion x < 0: SUCCESS \(unreachable\)$
|
||||
^\[f00.assertion.2\] .* assertion 1: SUCCESS \(unreachable\)$
|
||||
^\[f00.assertion.3\] .* assertion 0: SUCCESS \(unreachable\)$
|
||||
^\[f00.assertion.4\] .* assertion x >= 0: SUCCESS$
|
||||
^\[f00.assertion.5\] .* assertion x < 0: FAILURE \(if reachable\)$
|
||||
^\[f00.assertion.6\] .* assertion x < 2: FAILURE \(if reachable\)$
|
||||
^\[f00.assertion.7\] .* assertion \(x <= 0\) \? 1 : y: UNKNOWN$
|
||||
^\[f00.assertion.8\] .* assertion \(x <= 1\) \? 0 : y: UNKNOWN$
|
||||
^\[f00.assertion.9\] .* assertion \(x <= 2\) \? \(\(x <= 3\) \? 1 : 0\) : y: UNKNOWN$
|
||||
^\[f00.assertion.10\] .* assertion \(x <= 0\) \? 1 : y: UNKNOWN$
|
||||
^\[f00.assertion.11\] .* assertion \(x <= 1\) \? 0 : y: UNKNOWN$
|
||||
^\[f00.assertion.12\] .* assertion \(x <= 2\) \? \(\(x <= 3\) \? 1 : 0\) : y: UNKNOWN$
|
||||
^\[f00.assertion.13\] .* assertion \(x <= 0\) \? 1 : y: UNKNOWN$
|
||||
^\[f00.assertion.14\] .* assertion \(x <= 1\) \? 0 : y: UNKNOWN$
|
||||
^\[f00.assertion.15\] .* assertion \(x <= 2\) \? \(\(x <= 3\) \? 1 : 0\) : y: SUCCESS$
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
--
|
||||
^warning: ignoring
|
||||
--
|
||||
Tests the verify tasks handling of multiple traces for each assertion
|
||||
|
Loading…
Reference in New Issue