Overview of Map2Check
Map2Check Options
Contents
Map2Check Usage
Map2Check is invoked through a command-line interface as follows:
$./map2check [options] program.[i|c|bc]
To get a complete list of Map2Check’s command-line options run: map2check --help. The remainder of this page illustrate Map2Check’s main command-line options.
> > > v7.3.1-Flock : Wed Nov 27 20:38:14 UTC 2019 < < <
Usage: map2check [options] file.[i|c|bc]
Options:
--help show help
--version prints map2check version
--debug debug mode
--input-file arg specifies the files
--smt-solver arg (=z3) specifies the smt-solver, valid values are stp (STP),
z3 (Z3 is default), btor (Boolector), and yices2
(Yices)
--timeout arg timeout for map2check execution
--target-function searches for __VERIFIER_error is reachable
--generate-testcase creates c program with fail testcase (experimental)
--memtrack check for memory errors
--print-counter print counterexample
--memcleanup-property analyze program for memcleanup errors
--check-overflow analyze program for overflow failures
--check-asserts analyze program and verify assert failures
--add-invariants adding program invariants adopting Crab-LLVM
--generate-witness generates witness file
--expected-result arg specifies type of violation expected
--btree uses btree structure to hold information
(experimental, use this if you are having memory
problems)
Map2Check First Example
In this first example, we show how to apply Map2Check tool to identify a simple invalid free in the following C source code, called invalid_free.c
#include <stdio.h>
#include <stdlib.h>
int main()
{
int *a = malloc(12);
int *b = malloc(12);
int c = 12;
*a = c;
b = a;
free(a);
free(b);//invalid free
}
Map2Check should be called in the installation directory as follows: ./map2check invalid_free.c, this way the following result will be presented.
Started Map2Check Compiling /home/map2check/devel_tool/mygitclone/invalid_free.c Adding nondet pass Adding memtrack pass Adding map2check pass Linking with map2check library Instrumenting with LLVM LibFuzzer Executing LibFuzzer with map2check Running 2 workers ./5ee846f7dde256e515c97404b52edaee8239b686.map2check-fuzzed.out -use_value_profile=1 >fuzz-0.log 2>&1 ./5ee846f7dde256e515c97404b52edaee8239b686.map2check-fuzzed.out -use_value_profile=1 >fuzz-1.log 2>&1 ================== Job 0 exited with exit code 19712 ============ INFO: Seed: 1536959748 INFO: Loaded 1 modules (292 inline 8-bit counters): 292 [0x66f1a8, 0x66f2cc), INFO: Loaded 1 PC tables (292 PCs): 292 [0x45e1d0,0x45f410), INFO: -max_len is not provided; libFuzzer will not generate inputs larger than 4096 bytes ... Started counter example generation Counter-example: State 0: file /home/map2check/devel_tool/mygitclone/invalid_free.c ------------------------------------------------------------ >>Memory list log Line content : int *a = malloc(12); Address : 0x7f826bbf3e98 PointsTo : 0x7f82640009b0 Is Free : FALSE Is Dynamic : TRUE Var Name : Line Number : 6 Function Scope : main State 1: file /home/map2check/devel_tool/mygitclone/invalid_free.c ------------------------------------------------------------ >>Memory list log Line content : int *b = malloc(12); Address : 0x7f826bbf3e90 PointsTo : 0x7f8264000c40 Is Free : FALSE Is Dynamic : TRUE Var Name : Line Number : 7 Function Scope : main State 2: file /home/map2check/devel_tool/mygitclone/invalid_free.c ------------------------------------------------------------ >>Memory list log Line content : b = a; Address : 0x7f826bbf3e90 PointsTo : 0x7f82640009b0 Is Free : FALSE Is Dynamic : TRUE Var Name : Line Number : 10 Function Scope : main State 3: file /home/map2check/devel_tool/mygitclone/invalid_free.c ------------------------------------------------------------ >>Memory list log Line content : free(a); Address : 0x7f826bbf3e98 PointsTo : 0x7f82640009b0 Is Free : TRUE Is Dynamic : FALSE Var Name : Line Number : 12 Function Scope : main State 4: file /home/map2check/devel_tool/mygitclone/invalid_free.c ------------------------------------------------------------ >>Memory list log Line content : free(a); Address : 0x7f826bbf3e90 PointsTo : 0x7f82640009b0 Is Free : TRUE Is Dynamic : FALSE Var Name : Line Number : 12 Function Scope : main State 5: file /home/map2check/devel_tool/mygitclone/invalid_free.c ------------------------------------------------------------ >>Memory list log Line content : free(b);//invalid free Address : 0x7f826bbf3e90 PointsTo : 0x7f82640009b0 Is Free : TRUE Is Dynamic : FALSE Var Name : Line Number : 13 Function Scope : main ---------------------------------------------------- Violated property: file map2check_property line 13 function main FALSE-FREE: Operand of free must have zero pointer offset VERIFICATION FAILED
Map2Check Community
You are welcome to join us!
SUPPORT
Please send us an e-mail to map2check.tool@gmail.com for questions. You can submit bug reports, feature requests, or other issues via GitHub.
GITHUB
The Map2Check Tool source code is on GitHub. GitHub also hosts our Wiki and issue tracker.