Author: Herbert O. Rocha
E-mail: map2check.tool@gmail.com
================
.-.
/v\
// \\ > L I N U X - GPL <
/( )\
^^-^^
Goal:
Map2Check is a tool of automatically generating and checking memory management unit tests in C programs. The generation of unit tests is based on assertions extracted from safety properties generated by Bounded Model Checking tools. Map2Check checks for properties related to memory safety, such as: memory leaks and invalid free.
================
- Requirements for using the tool
To use this tool is necessary that the system contains the following software already installed properly:
- Linux OS
- Python (v2.7.1 or higher);
- Perl;
- GCC compiler;
- Pycparser (v2.10) - https://github.com/eliben/pycparser
- Pyparsing (v1.5.6) - http://pyparsing.wikispaces.com
- Networkx (v1.9.1) - https://networkx.github.io/
- Uncrustify (v0.60) - http://uncrustify.sourceforge.net
================
How to install Map2Check?
First of all, you need to install the required packages:
- STEP 0:
- Pycparser : $ pip install python-pycparser
- Pyparsing : $ pip install python-pyparsing
- Networkx : $ pip install python-networkx
- Uncrustify : $ apt-get install uncrustify
- STEP 1:
In order to install Map2Check on your PC, you should download and save the map2check.zip file on your disk. After that, you should type the following command:
$ unzip map2check.zip
or from https://github.com
$ git clone https://github.com/hbgit/Map2Check.git
- STEP 2:
Testing tool. Map2Check can be invoked through a standard command-line interface. Map2Check should be called in the installation directory as follows:
$ ./map2check.py code_samples/samples/false_free_2.c
For help and others options:
$ ./map2check.py -h
===========================
Instructions for SV-COMP'16
Use the 'map2check-wrapper.sh' script in the installation directory to verify each single test-case.
Usage:
$ ./wrapper_script_map2check.sh -c propertyFile.prp file.i.
Map2Check accepts the property file and the verification task and provides as verification result: FALSE(p) + Witness or UNKNOWN. FALSE(p), with p in {valid-free, valid-deref, valid-memtrack}, means that the (partial) property p is violated. For each error-path, a file that contains the violation path is generated in Map2Check root-path graphml folder; this file has the same name of the verification task with the extension graphml. There is timeout of 895 seconds set by this script, using "timeout" tool that is part of coreutils on debian and fedora. If these constraints are violated, it should be treated as UNKNOWN result.