PV4 ⊧ PredatorHP: Predator Hunting Partychecks memory-related errors and user-specified properties in C programsShape analyzer
- Memory-related errors
- Memory leaks
- Abstract interpretation
- C program to be verified, possibly with assertions
- Property file that contains the property that should be verified
- Path where witness file will be stored
- Optional: Compiler options
- C program:
.bcbitcode file. They provide instructions on how to generate the bitcode file from a C file.
- Property file:
.prpfile, same format as SV-COMP
- Path to witness file: Passed as argument when calling PredatorHP
- Optional compiler options: Passed as argument when calling PredatorHP
TRUE indicating that the specification is satisfied.
FALSE indicating that the specification is violated.
UNKNOWN if the tool could not determine whether the specification is satisfied or not.