This Branch adds features to Gazer, which are required for SV-Comp
Added features
Witness generation: SV-Comp requires a standard output format instead of trace.
Using the witness and hash flags, gazer can now generate a violation witness based on trace and a hardcoded correctness witness more about witnesses.
gazer_starter.py: A script, handling combined verification using gazer-bmc, gazer-theta and the generated test harnesses (the latter is for filtering incorrect false results).
Usage:./gazer_starter.py --output output_directory task.c(The output directory is for the witness and the test harness)(./gazer_start.py --version is also implemented)
Minor changes
In gazer-theta Theta is called with a bigger max heap and stack size. (Right now this is hardcoded, I'll open an issue about it for later)
The output format of version has been changed to be simpler and more similar to Theta.
Now it looks like this: Gazer v1.1.1 LLVM v9.0.0
The version number has been bumped up to v1.1.1 as well.
This Branch adds features to Gazer, which are required for SV-Comp
Added features
./gazer_starter.py --output output_directory task.c(The output directory is for the witness and the test harness) (./gazer_start.py --versionis also implemented)Minor changes
Gazer v1.1.1 LLVM v9.0.0The version number has been bumped up to v1.1.1 as well.