documentation.html

---
title: Arcana
layout: default
---
{% assign current = page.url | downcase | split: '/' %}
<!-- Main -->
<section class="wrapper style1">
	<div class="container">
		<div id="content">

				<!-- Content -->
			
					<div>
						<header>
							<h2>Overview of Map2Check</h2>
							<p>Map2Check Options</p>
						</header>                       
                       
                    <div style="width: 100%; margin-top: 100px;">
                        <p>Contents</p>
                        <ul>
                            <li>
                                <a href="#map_usage">Map2Check Usage</a>
                            </li>
                            <li>
                                <a href="#map_sample">Map2Check First Example</a>
                            </li>                            
                            <li>
                              <a href="#map_community">Map2Check Community</a>
                          </li>                            
                        </ul>
                        
                        <!-- Each content -->
                        <h2 id="map_usage">Map2Check Usage</h2>
                            <p style="text-align:justify">
                            Map2Check is invoked through a command-line interface as follows: 
                            </p>
<figure id="code">
<pre class="prettyprint lang-sh code">
$./map2check [options] program.[i|c|bc]
</pre>
</figure>
                            </br>
                            <p style="text-align:justify">
                            To get a complete list of Map2Check’s command-line options run: 
                            <font face="courier new"><a href="#map_options">map2check --help</a></font>. The remainder of this page illustrate Map2Check’s main command-line options.
                            </p>
<figure id="code">
<pre class="prettyprint lang-sh code">
> > > 	  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)
</pre>
</figure>
                            
                        <h2 id="map_sample">Map2Check First Example</h2>
                            <p style="text-align:justify">
                            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
                            </p>
<figure id="code">
<pre class="prettyprint lang-c linenums code">
#include &lt;stdio.h&gt;
#include &lt;stdlib.h&gt;

int main()
{
    int *a = malloc(12);
    int *b = malloc(12);
    int  c =  12;
    *a = c;
    b = a;
    
    free(a);
    free(b);//invalid free
}
</pre>
</figure>
                            </br>
                            <p style="text-align:justify">
                            Map2Check should be called in the installation directory as follows: 
                            <font face="courier new">./map2check invalid_free.c</font>, this way the 
                            following result will be presented. 
                            </p>
                            
<figure id="code">
<pre class="prettyprint lang-sh code">
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
</pre>
</figure>
</br>

<!-- Each content -->
<h2 id="map_community">Map2Check Community</h2>
<p style="text-align:justify">
You are welcome to join us!
</p>

<div style="width: 50px; float: left;"> 
  <i class="fas fa-headset fa-2x"></i> 
</div>
<div> 
  <h2>SUPPORT</h2>
</di>
<p style="text-align:justify">
Please send us an e-mail to map2check.tool@gmail.com for questions. 
You can submit bug reports, feature requests, or other issues via <a href="https://github.com/hbgit/Map2Check/issues">GitHub</a>. 
</p>


<div style="width: 50px; float: left;"> 
  <i class="fab fa-github fa-2x"></i> 
</div>
<div> 
  <h2>GITHUB</h2>
</di>
<p style="text-align:justify">
The Map2Check Tool source code is on <a href="https://github.com/hbgit/Map2Check">GitHub</a>. 
GitHub also hosts our <a href="https://github.com/hbgit/Map2Check/wiki">Wiki</a> and <a href="https://github.com/hbgit/Map2Check/issues">issue tracker</a>. 
</p>








</br>
                    </div>
		
			</div>
		</div>
	</section>