hbgit · WilliameRocha · Nov 17, 2016 · Nov 17, 2016 · Nov 30, 2016 · Nov 30, 2016
diff --git a/ALL.prp b/ALL.prp
diff --git a/README.md b/README.md
@@ -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 $ apt-get install default-jdk <br> Fedora $ sudo yum install java
+> - <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:

diff --git a/depthk-wrapper.sh b/depthk-wrapper.sh
@@ -1,10 +1,32 @@
 #!/bin/bash
+export PATH="$PATH:`pwd`"
+DEBUG_SCRIPT=0
+if [ $DEBUG_SCRIPT -eq 1 ]; then
+	echo "DepthK version"
+	./depthk.py --version
+	echo ""
+
+	ps axfl
+	cat /etc/lsb-release
+	uname -a
+	pwd
+
+	echo "GREP command: Testing 1 "
+	value=$( grep -c "depthk" depthk.py )
+	if [ "$value" -ge 1 ]
+	then
+	  echo "Grep works"
+	else
+	  echo "NOT works"
+	fi
+echo "DepthK version 3.0 - Mon Dez 19 17:40:02 AMT 2016"
+fi
+
 
 # ------------- DepthK wrapper script to tests
 # Usage: ./wrapper_script_tests.sh <[-p|]> <file.c|file.i>
 
 # ESBMC violation properties
-VIOLATED_PROPERTY_TAG="Violated property:"
 PROPERTY_FORGOTTEN_MEMORY_TAG="dereference failure: forgotten memory"
 PROPERTY_INVALID_POINTER_TAG="dereference failure: invalid pointer"
 PROPERTY_ARRAY_BOUND_VIOLATED_TAG="dereference failure: array bounds violated"
@@ -16,12 +38,9 @@ BENCHMARK_FALSE_VALID_DEREF="(${PROPERTY_INVALID_POINTER_TAG}|${PROPERTY_ARRAY_B
 
 # Benchmark result controlling flags
 IS_MEMSAFETY_BENCHMARK=0
-IS_TERMINATION_BENCHMARK=0
-
 # Path to the DepthK tool
 path_to_depthk="./depthk.py"
 
-
 # Memsafety cmdline picked
 do_memsafety=0
 do_term=0
@@ -31,83 +50,98 @@ property_list=""
 # Use parallel k-induction
 parallel=0
 
-passed_property_file=0;
 
-while getopts "c:mhp" arg; do
+
+while getopts "c:mhptv" arg; do
     case $arg in
         h)
             echo "Usage: $0 [options] path_to_benchmark
 Options:
 -h             Print this message
 -c propfile    Specifythe given property file
--p             Using k-induction with parallel algorithm"
+-p             Using k-induction with parallel algorithm
+-t             Testing a sample"
+exit
             ;;
         c)
             # Given the lack of variation in the property file... we don't
             # actually interpret it. Instead we have the same options to all
             # tests (except for the memory checking ones), and define all the
             # error labels from other directories to be ERROR.
             #if ! grep -q __VERIFIER_error $OPTARG; then
-            property_list=$OPTARG
-	    if grep -q -E "LTL[(]G \! overflow" $OPTARG; then
-		    do_overflow=1
-        fi
-
-	    if grep -q -E "LTL[(]G (valid-free|valid-deref|valid-memtrack)" $OPTARG; then
-                do_memsafety=1
-                IS_MEMSAFETY_BENCHMARK=1
-        fi
-
-	    if grep -q -E "LTL[(]F end" $OPTARG; then
-            	do_term=1
-                IS_TERMINATION_BENCHMARK=1
-        fi
+  	    cat $OPTARG > ./ALL.prp
+            property_list="./ALL.prp"
+	    echo "PRP: " "$property_list"
+            prp_overflow_result=$( grep -c "LTL(G[ ]*\![ ]*overflow" "$OPTARG")            
+			if [ "$prp_overflow_result" -ge 1 ]; then
+				do_overflow=1
+			fi
+
+			prp_mem_result=$( grep -c "LTL(G[ ]*(valid-free|valid-deref|valid-memtrack)" "$OPTARG")
+			if [ "$prp_mem_result" -ge 1 ]; then
+					do_memsafety=1
+					IS_MEMSAFETY_BENCHMARK=1
+			fi
+
+			prp_term_result=$( grep -c "LTL(F[ ]*" "$OPTARG")
+			if [ "$prp_term_result" -ge 1 ]; then
+					do_term=1
+			fi
         ;;
 	p) parallel=1
         ;;
+	t) getpwd=$( pwd )		
+		echo ""
+		prpfile="$getpwd/samples/ALL.prp"
+		opt_test="--debug --force-check-base-case --solver z3 --memlimit 15g --prp $prpfile  --extra-option-esbmc=\"--floatbv --no-bounds-check --no-pointer-check --no-div-by-zero-check --error-label ERROR\""
+		run_test="${path_to_depthk} $opt_test $getpwd/samples/example1_true-unreach-call.c"
+		result_check=$(timeout 895 bash -c "$run_test")
+		echo "$result_check"
+		exit
+        ;;
+	v) 
+
+		echo "DepthK version 3.0 - Mon Dez 19 17:40:02 AMT 2016"
+		exit	
+
+        ;;
     esac
 done
 
 if [ -z "$property_list" ]; then
    benchmark=${BASH_ARGV[0]}
-   directory=$(dirname $benchmark)
+   directory=$(dirname "$benchmark")
    possible_file="$directory/ALL.prp"
-   if [ -e $possible_file ]; then
-      if grep -q -E "LTL[(]G (valid-free|valid-deref|valid-memtrack)" $possible_file; then
+   if [ -e "$possible_file" ]; then
+      prp_mem_z_result=$( grep -c "LTL(G[ ]*(valid-free|valid-deref|valid-memtrack)" "$possible_file")
+	  if [ "$prp_mem_z_result" -ge 1 ]; then      
         do_memsafety=1
  	    IS_MEMSAFETY_BENCHMARK=1
       fi
-      if grep -q -E "LTL[(]F end" $possible_file; then
+      prp_term_z_result=$( grep -c "LTL(F[ ]*" "$possible_file")
+	  if [ "$prp_term_z_result" -ge 1 ]; then      
           do_term=1
-          IS_TERMINATION_BENCHMARK=1
       fi
    fi
 fi
 
-# Pick the command line to be using
-if test ${do_memsafety} = 0; then
-    cmdline=${global_cmd_line}
-else
-    cmdline=${memory_cmd_line}
-fi
-
 # Command line, common to all tests.
 depthk_options=""
 if test ${parallel} = 1; then
   if test ${do_memsafety} = 0; then
-    depthk_options="--debug --force-check-base-case --k-induction-parallel --solver z3 --memlimit 15g --extra-option-esbmc=\"--no-bounds-check --no-pointer-check --no-div-by-zero-check --error-label ERROR\""    
+    depthk_options=" --force-check-base-case --k-induction-parallel --solver z3 --memlimit 15g --prp "$property_list" --extra-option-esbmc=\"--no-bounds-check --no-pointer-check --no-div-by-zero-check --error-label ERROR\""    
   else
-    depthk_options="--debug --force-check-base-case --k-induction-parallel --solver z3 --memlimit 15g --memory-leak-check --extra-option-esbmc=\"--floatbv --error-label ERROR\""    
+    depthk_options="--force-check-base-case --k-induction-parallel --solver z3 --memlimit 15g --prp "$property_list" --memory-leak-check --extra-option-esbmc=\"--floatbv --error-label ERROR\""    
   fi
 else
     if test ${do_term} = 1; then
-	    depthk_options="--debug --force-check-base-case --solver z3 --memlimit 15g --termination-category --extra-option-esbmc=\"--floatbv --no-bounds-check --no-pointer-check --no-div-by-zero-check --error-label ERROR\""
+	    depthk_options="--force-check-base-case --solver z3 --memlimit 15g --termination-category --prp "$property_list" --extra-option-esbmc=\"--floatbv --no-bounds-check --no-pointer-check --no-div-by-zero-check --clang-frontend --error-label ERROR\""
 	elif test ${do_overflow} = 1; then
-	    depthk_options="--debug --force-check-base-case --solver z3 --memlimit 15g --overflow-check --extra-option-esbmc=\"--floatbv --no-bounds-check --no-pointer-check --no-div-by-zero-check --error-label ERROR\""
+	    depthk_options=" --force-check-base-case --solver z3 --memlimit 15g --overflow-check --prp "$property_list"  --extra-option-esbmc=\"--floatbv --no-bounds-check --no-pointer-check --no-div-by-zero-check --clang-frontend --error-label ERROR\""
     elif test ${do_memsafety} = 0; then
-        depthk_options="--debug --force-check-base-case --solver z3 --memlimit 15g --extra-option-esbmc=\"--floatbv --no-bounds-check --no-pointer-check --no-div-by-zero-check --error-label ERROR\""
+        depthk_options="--force-check-base-case --solver z3 --memlimit 15g --prp "$property_list" --extra-option-esbmc=\"--floatbv --no-bounds-check --no-pointer-check --no-div-by-zero-check --clang-frontend --error-label ERROR\""
     else
-        depthk_options="--debug --force-check-base-case --solver z3 --memlimit 15g --memory-safety-category --extra-option-esbmc=\"--floatbv --memory-leak-check --error-label ERROR\""
+        depthk_options="--force-check-base-case --solver z3 --memlimit 15g --prp "$property_list" --memory-safety-category --extra-option-esbmc=\"--floatbv --memory-leak-check --clang-frontend --error-label ERROR\""
     fi
 fi
 
@@ -122,95 +156,46 @@ if test "${benchmark}" = ""; then
     exit 1
 fi
 
-
-# Creating Dir to save the logs
-#LOGS_depthk="LOGS_depthk"
-#if [ ! -d "$LOGS_depthk" ]; then
-#    mkdir "$LOGS_depthk"
-#fi
-
-
 # The complete command to be executed
 run_cmdline="${path_to_depthk} ${depthk_options} \"${benchmark}\";"
 #echo "$run_cmdline"
 #exit
 # Invoke our command, wrapped in a timeout so that we can
 # postprocess the results. `timeout` is part of coreutils on debian and fedora.
-result_check=`timeout 895 bash -c "$run_cmdline"`
-
-# Saving logs
-echo "$result_check" &> "${benchmark}"".log"
-# mv "${benchmark}"".log" "$LOGS_depthk"
-# Getting K adopted by ESBMC
-bound="-"
-bond_check1=`tac  "${benchmark}"".log" | grep -o "^\*\*\* K-Induction Loop Iteration.*" | grep -o "[0-9]*[^ ]*" -m 1`
-if [ ! -z "$bond_check1" ]; then
-   bound=$bond_check1
-else 
-	bond_check2=`tac  "${benchmark}"".log" | grep -o "^Unwinding loop.*" | grep -o "iteration[ ]*[0-9]*[^ ]*" | grep -o "[0-9]*$" -m 1`
-	if [ ! -z "$bond_check2" ]; then
-		bound=$bond_check2
-	else
-		bond_check3=`tac  "${benchmark}"".log" | grep -o "^MAX k (100) reached." -m 1`
-		if [ ! -z "$bond_check3" ]; then
-			bound="50"
-		fi
-	fi
-fi
-
-# Getting step of the verification
-step="-"
-step_check=`tac  "${benchmark}"".log" | grep -o "Status: checking.*" -m 1 | sed -e  "s/Status: checking //"`
+result_check=$(timeout 895 bash -c "$run_cmdline")
 
-if [ ! -z "$step_check" ]; then
-   step=$step_check
+if [ $DEBUG_SCRIPT -eq 1 ]; then
+	echo "${result_check}"
 fi
 
-#echo "Solution by:$step"
-rm "${benchmark}"".log"
-
-
-# Identify problems with invariants generation
-# Not supported by PIPS
-#PIPSerror=`echo ${result_check} | grep -c "A problem was identified in PIPS"`
-# When it is not possible generate the invariants
-#invTO=`echo ${result_check} | grep -c "TIMEOUT to generate the invariants"`
-
-# Checking approach to force last check with base case
-#forcelastcheckbc=`echo ${result_check} | grep -c "> Forcing last check in base case"`
-
-
-# Postprocessing: first, collect some facts
-#echo ${run_cmdline}
-
 VPROP=""
 
 if test ${IS_MEMSAFETY_BENCHMARK} = 1; then
 
-   false_valid_mamtrack=`echo ${result_check} | grep -c "${BENCHMARK_FALSE_VALID_MEMTRACK}"`
-   false_valid_deref=`echo ${result_check} | grep -c "${BENCHMARK_FALSE_VALID_DEREF}"`
+   false_valid_mamtrack=$(echo "${result_check}" |grep -c "${BENCHMARK_FALSE_VALID_MEMTRACK}")
+   false_valid_deref=$(echo "${result_check}" |grep -c "${BENCHMARK_FALSE_VALID_DEREF}")
 
-   if [ $false_valid_mamtrack -gt 0 ]; then
+   if [ "$false_valid_mamtrack" -gt 0 ]; then
       VPROP=$"(valid-memtrack)"
-   elif [ $false_valid_deref -gt 0 ]; then
+   elif [ "$false_valid_deref" -gt 0 ]; then
       VPROP=$"(valid-deref)"
    fi
 elif test ${do_overflow} = 1; then
     VPROP=$"(no-overflow)"
 fi
 
-failed=`echo ${result_check} | grep -c "FALSE"`
-success=`echo ${result_check} | grep -c "TRUE"`
+failed=$(echo "${result_check}" |grep -c "FALSE")
+success=$(echo "${result_check}" |grep -c "TRUE")
 
 # Decide which result we determined here.
-if [ $failed -gt 0 ]; then
+if [ "$failed" -gt 0 ]; then
     # Error path found
     if test ${do_term} = 1; then
        echo "UNKNOWN"
     else
        echo "FALSE${VPROP}"
     fi
-elif [ $success -gt 0 ]; then
+elif [ "$success" -gt 0 ]; then
     echo "TRUE"
 else
     echo "UNKNOWN"