---------------------------- FORTES TOOL (Beta) v2.1 -------------------------------

		  .-.
		  /v\
		 // \\    > L I N U X - GPL <
		/(   )\
		 ^^-^^
__________________________________________________________________________________________________________________
		
Goal: 
This tool aims to automate the FORTES method that aims to automate to extract the safety properties from C code generated by ESBMC to generate automatically testcases using the assertions, in this case adopting the CUnit Framework Unit Test.

Author: Herbert O. Rocha E-mail: [email protected]

Version: 2.1 Beta - Year: 2012

Status: This tool is still in development phase to full implementation of the proposed method in this approach.
_____________________________________________________________________________________________________________________

-> Requirements for using the tool
_____________________________________________________________________________________________________________________

To use this tool is necessary that the system contains the following software already installed properly:

- Perl;
- CUnit available at http://cunit.sourceforge.net;
- Shell Script;
- And the ESBMC model checker, which you should set the environment variable PATH in your .bashrc.
_____________________________________________________________________________________________________________________

-> How to install ESBMC?
_____________________________________________________________________________________________________________________

The ESBMC can be downloaded at http://esbmc.org/

In order to install ESBMC on your PC, you should download and save the esbmc-vx.x.tar.gz file on your disk. 
After that, you should type the following command:

$ tar -xzvf esbmc-v1.12.tar.gz

The ESBMC distribution is split into three directories:

- bin
- smoke-tests
- licenses

The directory bin contains the binary file of ESBMC. The directory smoke-tests contains some ANSI-C programs and also 
includes a shell script that can be used to collect experimental results for different ANSI-C benchmarks 
(e.g., check the encoding time, decision procedure time, total number of lines of code, total number of properties 
to be verified, how many properties passed, violated and failed during the verification process).

You should set the environment variable PATH in your .bashrc file as follows:

$ export PATH=$PATH:/home/herbert/esbmc-vx.x/bin/
_____________________________________________________________________________________________________________________

-> How to install FORTES?
_____________________________________________________________________________________________________________________

In order to install FORTES on your PC, you should download and save the fortes_vx.tar.gz file on your disk. 
After that, you should type the following command:

>> STEP 1:

$ tar -xzvf fortes_vx.tar.gz

The FORTES distribution is split into directories and files:

- code_samples (Samples codes to apply FORTES) 
- modules
  - get_and_set_claims
  - preprocessor
	- aux_preprocessing (Could not to finish yet)	
	- primary_preprocessing
- result_claims
- README  
- fortes.sh 
- config.sh

>> STEP 2:

Open the directory where the FORTES tool was extracted and then you should locate the config.sh and fortes script. After that, you should run the config.sh script, it is worth to say that you should run the config.sh script from inside the directory where FORTES was extracted.

Example:

1) $ cd fortes_vx
2) $ ls
	code_samples  <config.sh>  <fortes>  modules  README  result_claims
3) $ ./config.sh


>> STEP 3:

It is advisable that you should set the environment variable PATH in your .bashrc file as follows:

$ export PATH=$PATH:/home/user/fortes_vx/

>> STEP 4:

Testing FORTES

$ fortes code_samples/D_CBMC_bound_array.c > out_code.c

>> STEP 5:

Running CUnit code

$ gcc out_code.c -o out_code -lcunit

_____________________________________________________________________________________________________________________

-> How running the FORTES?
_____________________________________________________________________________________________________________________

Running FORTES.

$ fortes <file.c>

For help and others options:

$ ./fortes.sh -h
_____________________________________________________________________________________________________________________
---------------------------------------------------------------------------------------------------------------------