Added Jahob from svn repository on larasvn

COPYING.MIT

@@ -0,0 +1,12 @@
+Copyright (c) 2005, 2006 
+  Viktor Kuncak ([email protected])
+  Thomas Wies ([email protected])
+  Karen Zee ([email protected])
+  Huu Hai Nguyen ([email protected])
+  Peter Schmitt ([email protected])
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

INSTALL

@@ -0,0 +1,125 @@
+Jahob preliminary version of 20 August 2012.
+
+This version corrects several bugs and adds several capabilities contributed by
+Alexander Malkis. The main of them are:
+- the switch "-tryHard" for a further aggressive splitting of verification
+  conditions.
+- handling cardinalities of comprehensions of finite sets before calling 
+  a decision procedure for BAPA.
+
+Required:
+make, version >= 3.81
+ocaml, version >= 3.12.1
+gcc, version >= 4.6.2
+Recommended:
+mona, version >= v1.4-13
+spass, version >= 3.7
+cvc3, version >= 2.2
+z3, version >= 3.2
+
+Compilation:
+vim lib/cudd/Makefile
+# adapt XCFLAGS for your machine
+cd src
+make clean && make depend && make all
+
+------------------------------------------------------------
+Jahob preliminary version of 8 April 2007.
+
+This distribution is meant for students of the EPFL class 
+Software Analysis and Verification 2007, taught by Viktor Kuncak.
+
+It contains simpler make files for formDecider, namely
+Makefile.formDecider and Makefile.formDecider.opt.
+
+On the technical side it contains many important improvements of the
+underlying analyses and decision procedures which have not all been
+documented yet and should not be relied on or reverse engineered.
+
+------------------------------------------------------------
+Jahob preliminary version of 23 July 2006.
+
+This version adds the following key improvements implemented by 
+  Charles Bouillaguet that joins the Jahob team:
+
+  * TPTP interfaces to first-order theorem provers
+  * SPASS interface (works with SPASS 3.7)
+       (try downloading executables with as eprover and SPASS)
+  * Coq interface
+  * complete hiding of objects
+
+It also incorporates numerous improvements for Bohne, developed
+by Thomas Wies, and a new version of verification condition generator
+written by Viktor Kuncak, invoked by -sastvc.
+
+There are other features and changes that are currently not
+documented, but we decided to release the updated sources
+anyway.  Documentation should appear in a few months at
+most.  We have more extensive set of libraries and a
+regression suite that you can run
+
+------------------------------------------------------------
+
+Jahob preliminary version of 1 February 2006.
+
+This is a preliminary distribution.
+Please let us know if you are planing to use it.
+More installation friendly distribution might come soon.
+
+(c) Viktor Kuncak ([email protected])
+    Thomas Wies ([email protected])
+    Karen Zee ([email protected])
+    Huu Hai Nguyen ([email protected])
+    Peter Schmitt ([email protected])
+
+The wrote written by us is released under GPL and MIT
+licence (make your pick), see files COPYING.* .  We are using
+Caddie, which you can use under their own licences.
+
+MIT licence should allow any reasonable use of this system, but let us
+know if you have a problem.
+
+Instalation instructions (verified under Debian distribution with kernel
+Linux 2.6.8-1-686-smp #1 SMP Thu Nov 25 04:55:00 UTC 2004 i686 GNU/Linux).
+
+Required:
+  make
+  ocaml distribution (tested with ocamlc version 3.09.1)
+
+Instalation instructions: 
+  Untar the distribution
+  Type make to create bytecode compiled versions
+    This will produce executable bin/jahob directory
+  Type 
+     cd src; make -f Makefile.opt depend; make -f Makefile.opt ../bin/jahob.opt
+     This will produce native code compiled executables.
+
+  We run executables by doing cd into the appropriate example subdirectory
+  and then running something like:
+
+    ../../../bin/jahob JavaFile1.java JavaFile2.java -method JavaFile1.methodName -nobackground -usedp mona isa cvcl
+
+  Executables will place their temporary files in
+  the ../tmp/ directory relative
+  to where their position.
+
+Jahob can use the following external programs 
+(with the corresponding executable names):
+
+ MONA - used for analyzing linked data structures
+   http://www.brics.dk/mona/
+
+ Isabelle cvs snapshot from 24 February 2005 - useful fallback
+   http://www4.informatik.tu-muenchen.de/~isabelle/
+
+ CVC Light (or other SMT-LIB compatible prover; we only tested it with CVCL)
+   http://chicory.stanford.edu/CVCL/
+
+ Simplify, not essential (Simplify)
+   only minimal support
+
+ Omega Calculator (oc)
+   http://www.cs.umd.edu/projects/omega/
+
+ LASH executable, not essential (presburger)
+   - an alternative for Omega, usually worse

Makefile

@@ -0,0 +1,5 @@
+all:
+	cd src; \
+	make clean; \
+	make depend; \
+	make all