PV4 ⊧ PredatorHP: Predator Hunting Partychecks memory-related errors and user-specified properties in C programs

Shape analyzer

Application domain/field

• Memory-related errors
• Memory leaks
• Abstract interpretation

Expected input

• 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

Format:

• C program: .bc bitcode file. They provide instructions on how to generate the bitcode file from a C file.
• Property file: .prp file, same format as SV-COMP
• Path to witness file: Passed as argument when calling PredatorHP
• Optional compiler options: Passed as argument when calling PredatorHP

Expected output

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.

Internals

PredatorHP is built on the Predator shape analyzer. PredatorHP looks for memory-related errors such as invalid pointer dereferences, double free operations and memory leaks. It also checks the validity of assertions in the code. PredatorHP runs multiple tools in parallel. The first tool is the Predator verifier, which can claim that a program is correct. The other tools are called hunters, which typically report errors. These hunters are used to decrease the chances of producing false alarms. TACAS'20: improved handling of interval-sized memory regions or new support of memory reallocation

Comments

License: GPL v3.0