Map2Check is a bug hunting tool that automatically generating and checking safety properties in C programs. It tracks memory pointers and variable assignments to check user-specified assertions, overflow, and pointer safety. The generation of the tests cases are based on assertions (safety properties) from the code instructions, adopting the LLVM framework version 6.0, LibFuzzer, KLEE to generate input values to the test cases generated by Map2Check. Additionally, we have adopted Crab-LLVM tool to computes inductive invariants for LLVM-based languages.
Extra documentation is available at https://map2check.github.io
To use the Map2Check tool is necessary a Linux 64-bit OS system. In the linux OS, you should install the requirements, typing the commands:
$ sudo apt install python-minimal
$ sudo apt install libc6-devOur binary tool is avaliable at https://github.com/hbgit/Map2Check/releases
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-rc-v7.3-svcomp20.zip
$ cd map2check-rc-v7.3-svcomp20Map2Check can be invoked through a standard command-line interface. Map2Check should be called in the installation directory as follows:
$ ./map2check --memtrack svcomp_960521-1_false-valid-free.cIn this case, --memtrack is the option to check for memory errors. For help and others tool options:
$ ./map2check --helpWhen you use a LLVM bytecode as input for the tool, be sure to add -g flag when generating the file, it is not required, but map2check will provide better info (like line numbers).
You can build Map2Check using our Dockerfile by clone our repository:
$ git clone https://github.com/hbgit/Map2Check.git
$ cd Map2Check
$ git submodule update --init --recursive
# Build docker image to compile Map2Check
$ docker build -t hrocha/mapdevel --no-cache -f Dockerfile .
$ docker run --rm -v $(pwd):/home/map2check/devel_tool/mygitclone:Z --user $(id -u):$(id -g) hrocha/mapdevel /bin/bash -c "cd /home/map2check/devel_tool/mygitclone; ./make-release.sh; ./make-unit-test.sh"More details at https://map2check.github.io/docker.html
You should build the Benchexec docker image that is available in our repository in the submodule:
$ cd Map2Check
$ docker build -t hrocha/benchexecrun --no-cache -f utils/benchexecrun/Dockerfile utils/benchexecrun/
# Running the regression testing
$ ./make-regression-test.sh tUse the map2check-wrapper.py script in the Map2Check binary directory to verify each single test-case.
Usage:
$ ./map2check-wrapper.py -p propertyFile.prp file.iMap2Check 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, valid-memcleanup}, 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 897 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.
Maintainers:
- Herbert O. Rocha (since 2014), Federal University of Roraima, Brazil - https://hbgit.github.io/
- Rafael Menezes (since 2016), Federal University of Roraima, Brazil - https://rafaelsa94.github.io/
Questions and bug reports:
E-mail: [email protected]
.-.
/v\
// \\ > L I N U X - GPL <
/( )\
^^-^^
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent