================
Goal:
Map2Check is a tool of automatically generating and checking memory management tests cases in C programs. The generation of the tests cases are based on assertions (safety properties) from the code instructions, adopting the LLVM framework and KLEE tool to generate input values to the test cases generated by Map2Check. Map2Check checks memory safety properties, such as: invalid deference, invalid free, and memory leaks.
Documentation available at https://map2check.github.io
================
- Requirements for using the tool
To use this tool is necessary a Linux OS system. Our binary tool is avaliable at https://github.com/hbgit/Map2Check/releases
================
How to build Map2Check?
You can build Map2Check using our dockerfile, more details at https://map2check.github.io/docker.html
Install Map2Check
In order to install Map2Check on your PC, you should download and save the map2check zip file on your disk from https://github.com/hbgit/Map2Check/releases. After that, you should type the following command:
$ unzip map2check_v7.1_svcomp.zip $ cd Map2Check-map2check_v7.1_svcomp
Testing tool
Map2Check can be invoked through a standard command-line interface. Map2Check should be called in the installation directory as follows:
$ ./map2check sample/svcomp_960521-1_false-valid-free.c
For help and others options:
$ ./map2check --help
===========================
Instructions for SV-COMP'18
Use the 'map2check-wrapper.py' script in the installation directory to verify each single test-case.
Usage:
$ ./map2check-wrapper.py -p propertyFile.prp file.i
Map2Check accepts the property file and the verification task and provides as verification result: TRUE + Witness, [FALSE|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 verification result the witness file (called witness.graphml) is generated Map2Check root-path folder. There is timeout of 895 seconds set by this script, using "timeout" tool that is part of coreutils on debian. If these constraints are violated, it should be treated as UNKNOWN result.
===========================
Authors
Maintainers:
Herbert O. Rocha (since 2014), Federal University of Roraima, Brazil
Rafael Menezes (since 2016), Federal University of Roraima, Brazil
Questions and bug reports:
E-mail: map2check.tool@gmail.com
.-.
/v\
// \\ > L I N U X - GPL <
/( )\
^^-^^