herberthb/map2check repository overview

⁠Map2Check

⁠A Software Verification based on Test Cases Generation of C Programs

================

Goal:

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](http://llvm.org/) and [LibFuzzer](https://llvm.org/docs/LibFuzzer.html) to generate input values to the test cases generated by Map2Check.

Extra documentation is 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](../../../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:

Testing tool

Map2Check can be invoked through a standard command-line interface. Map2Check should be called in the installation directory as follows:

For help and others options:

===========================

Instructions for SV-COMP'18

Use the 'map2check-wrapper.py'⁠ script in the 'utils' directory to verify each single test-case.

Usage:

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: [email protected]⁠

      .-.          
      /v\
     // \\    > L I N U X - GPL <
    /(   )\
     ^^-^^