verison upgraded

README.md

@@ -1,4 +1,4 @@
-<h1>DepthK 3.0</h1>
+<h1>DepthK 3.1</h1>
 <h3>K-Induction adopting program invariants</h3>
 
 ================ 
@@ -16,13 +16,16 @@ To use this tool is necessary that the system contains the following software al
 
 > - Linux OS
 > - Python (v2.7.1 or higher);
-> - sed;
-> - grep;
-> - GCC compiler; 
 > - Uncrustify (v0.60 or higher) - http://uncrustify.sourceforge.net/
 > - Pycparser (v2.10) - https://github.com/eliben/pycparser
 > - Ctags - http://ctags.sourceforge.net 
+> - Clang (v3.5) - http://clang.llvm.org
 > - PIPS - http://pips4u.org
+> - sed
+> - grep
+> - timeout
+> - GCC compiler
+> - Java (v1.7 or higher);
 
 ==============
 
@@ -36,8 +39,11 @@ First of all, you need to install the required packages:
 
 > - <b>Uncrustify</b>: <br> Ubuntu $ sudo apt-get install uncrustify <br> Fedora $ sudo yum install uncrustify
 > - <b>Pycparser</b>: <br> Ubuntu $ sudo apt-get install python-pycparser <br> Fedora $ sudo yum install python-pycparser
-> - <b>Ctags</b>: <br> Ubuntu $ sudo apt-get install exuberant-ctags <br>Fedora $ sudo yum install ctags
-> - <b>PIPS</b>: <br>Available at http://pips4u.org/copy_of_getting-pips/building-and-installing-pips-from%20svn <br>
+> - <b>Ctags</b>: <br> Ubuntu $ sudo apt-get install exuberant-ctags <br> Fedora $ sudo yum install ctags
+> - <b>Clang</b>: <br> Ubuntu $ sudo apt-get install clang-3.5 <br> Fedora $ sudo yum install clang-3.5
+> - <b>GCC</b>: <br> Ubuntu $ sudo apt-get install gcc <br> Fedora $ sudo yum groupinstall "Development Tools"
+> - <b>Java</b>: <br> Ubuntu $ sudo apt-get install openjdk-8-jre <br>
+> - <b>PIPS (optional)</b>: <br>Available at http://pips4u.org/copy_of_getting-pips/building-and-installing-pips-from%20svn <br>
 You should set the environment variable PATH in your .bashrc file. <br> 
 Checkout Step 4: Load the PIPS environment variables from that link<br>
 
@@ -59,27 +65,16 @@ or from https://github.com
 
 <p align="justify">
 Testing tool. DepthK can be invoked through a standard command-line interface. DepthK should be called 
-in the installation directory as follows:  
-</p>
-
-> $ ./depthk.py samples/conceptproof/invgen/confuse/confuse.c -g <br> 
-> \>\> Running PIPS to generate the invariants <br>
-> \>\> Translating the PIPS annotation with the invariants <br>
-> \>\> Starting the verification of the P' program <br>
-> 	 \-\> Actual k = 1 <br>
-> 		 Status: checking base case <br>
-> 		 Status: checking forward condition <br>
-> 		 Status: checking inductive step <br>
-> TRUE <br>
-
+in the installation directory. For help and others options: 
 
-By default ESBMC is called, as follows: 
-> $ ./esbmc --64 --no-library --z3 --unwind \<nr\> --timeout 15m [--base-case|--forward-condition|--inductive-step] <file.c>
+> $ ./depthk.py --help
 
-For help and others options: 
+</p>
 
-> $ ./depthk.py --help
+Use the 'depthk-wrapper.sh' script in the installation directory to verify each single test-case:
 
+> $ ./depthk-wrapper.sh -c  /home/user/depthk/samples/ALL.prp /home/user/depthk/samples/example1_true-unreach-call.c <br>
+> TRUE <br>
 
 
 ===========================
@@ -90,7 +85,7 @@ Use the 'depthk-wrapper.sh' script in the installation directory to verify each
 
 Usage: 
 
-> $ ./wrapper_script_tests.sh <[-p|]>  file.i
+> $ ./depthk-wrapper.sh -c  full/path/propertyFile.prp full/path/file.i
 
 <p align="justify">
 DepthK provides as verification result: