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:

• properties.txt: to save the property to be checked;
• allPointers.txt: to save all the pointers in C programs when checking null pointer dereference. Note that in CTPChecker, we also developed a module to support automic property formalizing for checking null pointer dereference in C programs.
• proposition.txt: to save the corresponding predicates.

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