PV4 ⊧ Map2Checkchecks user-specified properties, overflows and memory-safety of C programs

Map2Check is a bug hunting tool that automatically checks safety properties in C programs

Application domain/field

• Fuzzing
• Symbolic execution
• Inductive invariants
• Safety properties
• Unit tests
• Assertions
• Memory safety

Expected input

• C program
• Property file

Format:

• C program: .c file
• Property file: .prp file (SV-COMP format)

Expected output

TRUE + witness, FALSE or FALSE(p) + witness or UNKNOWN. FALSE(p) means that the property p is violated.

Internals

Map2Check checks for the following (SV-COMP) properties:

• Invalid free
• Invalid dereference
• Memory leak
• Assertion violations
• Overflows
• Pointer safety

Uses KLEE, LibFuzzer, Crab-LLVM

Comments

License: GPL v2.0