TPChecker is a tool for verifying temporal properties of C programs.
Download and Installation:
The tool is available at (1, 2, 3, 4) . The platform is windows OS and Eclipse. First, you need to install a Java Runtime Environment which is at least Java 7 compatible. Second, you need to create a folder D:property, and put the following three files inside it:
How to use?
1. Choose a source code file (C program) that you want to check.
2. Choose a configuration file. Standard configuration files can be found in the directory config/. These are two extended configuration files, predicateAnalysis-PredAbsRefiner-SBE-pointer.properties and predicateAnalysis-PredAbsRefiner-SBE-simpleproperty.properties.
3. Write the property to D:propertyproperties.txt and the propisitions to D: propertypropositions.txt.
Note that if you check the null pointer dereference, the property can be created automatically. So, you don’t need to write it to the file D:propertypropositions.txt.
4. Execute the command "sc[ant]ripts/cpa.bat [ -config <CONFIG_FILE> ] <SOURCE_FILE>", e.g. sc[ant]ripts/cpa.bat -config config/predicateAnalysis PredAbsRefiner-SBE-pointer.properties example.c