Now directly test individual lines with perls regex matching rather than
calling out to grep. Some changes were required:
- escape (, ) if we want to match them
- unescape (, ) if we want to use them as regex bracket groups
- escape +, $ if we want to use them as actual characters
- unescape + to use as a regex +
Includes tests for excluded lines and multi lines.
Includes tests that the test runner should fail, these are set as KNOWNBUG
so we can run the regressions folder.
We also don't print out when grep options activated as no chance of doing
by accident as very clearly different to any other syntax. The printing
messes up the formatting of the output so better to not have it.
Added test script to the Makefile
Also ordered the tests into alphabetical orde.r
To correctly unwind static inits of Java enums, one first has to check whether
the function is actually a Java function. This patch also adds a first
regression test for static loop unwinding.
Fixes: b49a7fc3a3
The first five of these are split up pieces of the existing
instanceof1, and the final two are new.
The first three (testing array and primitive classids) don't
work at present; those dealing with ordinary reference types (3-7)
do.
For member accesses, access to other components need not be valid as
shown in the included regression test Malloc23.
Also do not require --bounds-check for full dereferencing checks.
Fixes#219.
Previously checking against malloc bounds and against statically-bounded arrays (e.g. int[2]) were mutually exclusive. This enables the static array bounds check even for dynamic objects.
Fixes#239.
Added cases for union types, for anonymous structs and for volatile
variables (as opposed to const variables). Also added test for verifying
the dump C output
The known bug related to this issue was checking the output was wrong,
so made it check the correct output. Since it is now fixed, swapped it
from KNOWNBUG to CORE.
This creates three source-level variables that are
notionally live for the whole function, but then uses
the function's dominator tree information to show that
they actually have disjoint scopes. Similarly the
temporary used to hold a new instance between creation
and assignment to a local variable should be given
a bounded scope.
Nondet was added too late in _start, leading to a new nondet solution at
each CEGIS counterexample loop iteration. The bug was not present in the
verification phase, hence any solution produced by this was still sound.
However, this severely affects CEGIS' ability to find adequate solutions
and worst case leads to a "same counterexample" assertion violation.
Daniel Kroening