From 70194baa133d2d0dedd38b499727f6ad4214c5d8 Mon Sep 17 00:00:00 2001
From: "o.elhawi@gmail.com"
Testing tool. DepthK can be invoked through a standard command-line interface. DepthK should be called
-in the installation directory as follows:
-DepthK 3.0
+DepthK 3.1
K-Induction adopting program invariants
================
@@ -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:
> - Uncrustify:
Ubuntu $ sudo apt-get install uncrustify
Fedora $ sudo yum install uncrustify
> - Pycparser:
Ubuntu $ sudo apt-get install python-pycparser
Fedora $ sudo yum install python-pycparser
-> - Ctags:
Ubuntu $ sudo apt-get install exuberant-ctags
Fedora $ sudo yum install ctags
-> - PIPS:
Available at http://pips4u.org/copy_of_getting-pips/building-and-installing-pips-from%20svn
+> - Ctags:
Ubuntu $ sudo apt-get install exuberant-ctags
Fedora $ sudo yum install ctags
+> - Clang:
Ubuntu $ sudo apt-get install clang-3.5
Fedora $ sudo yum install clang-3.5
+> - GCC:
Ubuntu $ sudo apt-get install gcc
Fedora $ sudo yum groupinstall "Development Tools"
+> - Java:
Ubuntu $ sudo apt-get install openjdk-8-jre
+> - PIPS (optional):
Available at http://pips4u.org/copy_of_getting-pips/building-and-installing-pips-from%20svn
You should set the environment variable PATH in your .bashrc file.
Checkout Step 4: Load the PIPS environment variables from that link
@@ -59,27 +65,16 @@ or from https://github.com
-> \>\> Running PIPS to generate the invariants
-> \>\> Translating the PIPS annotation with the invariants
-> \>\> Starting the verification of the P' program
-> \-\> Actual k = 1
-> Status: checking base case
-> Status: checking forward condition
-> Status: checking inductive step
-> TRUE
-
+in the installation directory. For help and others options:
-By default ESBMC is called, as follows:
-> $ ./esbmc --64 --no-library --z3 --unwind \
DepthK provides as verification result: