Add bounded box domain

.gitignore

@@ -1,12 +1,17 @@
 *~
+
+# sbt-specific
 target/
-.project
-.cache
+
+# eclipse
 .classpath
-.worksheet
-.history
-*.sc
+.worksheet/
 .settings/
+.project
+target.eclipse/
+.cache-main
+.cache-tests
+*.sc
+*.log
+# intellij idea
 .idea/
-.cache-*
-

.travis.yml

@@ -0,0 +1,6 @@
+language: scala
+scala:
+   - 2.12.4
+
+script:
+  - sbt test

build.sbt

@@ -1,54 +1,67 @@
+import CustomKeys._
+
 //*** Declare projects
 
-val Jandom = project in file("core") enablePlugins(BuildInfoPlugin)
+lazy val JandomCore = project in file("core") enablePlugins(BuildInfoPlugin)
+
+lazy val JandomExtended = project in file("extended") dependsOn JandomCore % "compile->compile;test->test"
+
+lazy val Jandom = project in file(".") aggregate (JandomCore, JandomExtended) 
+
+//*** This delegates the Jandom run task to execute the run task in the Jandom sub-projects
 
-val JandomExtended = project in file("extended")  dependsOn Jandom % "compile->compile;test->test"
+aggregate in assembly := false
 
-val root = project in file(".")  aggregate (Jandom, JandomExtended) 
+assembly := (assembly in JandomExtended).value
 
-// This delegates the root run task to the run task in the Jandom project
+run := (run in JandomCore in Compile).evaluated
 
-run <<= run in ("Jandom", Compile)
+run in Test := (run in JandomCore in Test).evaluated
 
-run in Test <<= run in ("Jandom", Test)
+run in Jmh := (run in JandomExtended in Jmh).evaluated
 
-// Add a new benchmark configuration...
-// val Bench = config("bench") extend(Test)
-// val root = project in file(".") configs(Bench) settings( inConfig(Bench) (Defaults.testSettings):_*) aggregate (Jandom, JandomExtended) 
+//*** Do not update snapshots every time
+
+updateOptions in ThisBuild := updateOptions.value.withLatestSnapshots(false)
 
 //*** Scala configuration
 
-scalaVersion in ThisBuild := "2.11.8"
+scalaVersion in ThisBuild := "2.12.3"
 
-scalacOptions in ThisBuild ++= Seq("-deprecation", "-feature", "-Xlint", "-Xlint:-delayedinit-select", "-Xlint:-missing-interpolator")
+scalacOptions in ThisBuild ++= Seq("-deprecation", "-feature", "-unchecked", "-Xlint:_,-missing-interpolator", "-Ywarn-unused:-implicits")
 
 fork in ThisBuild := true
 
 //*** Resolvers
 
-resolvers in ThisBuild ++= Seq(
+resolvers in ThisBuild ++= Seq (
   Resolver.sonatypeRepo("releases"),
-  Resolver.sonatypeRepo("snapshots")
+  Resolver.sonatypeRepo("snapshots"),
+  "Soot snapshot" at "https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/",
+  "Soot release" at
+   "https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/"
 )
 
-//*** Detect PPL
+//*** Custom keys
 
-val optionalPPLPathName = try {
-    val PPLPathName = Process("ppl-config -l").lines.head+"/ppl/ppl_java.jar"
+pplJar in ThisBuild := {
+  try {
+    val PPLPathName = scala.sys.process.Process("ppl-config -l").lineStream.head+"/ppl/ppl_java.jar"
     if (file(PPLPathName).exists) Some(PPLPathName) else None
   } catch {
     case _ : Exception => None 
   }
+}
+
+gitHeadCommitSHA in ThisBuild := scala.sys.process.Process("git rev-parse HEAD").lineStream.head
+
+//*** Eclipse plugin
 
-pplJar in ThisBuild := optionalPPLPathName
+// unfortunately, it is not possible to choose the compiler version with the eclipse plugin.
 
-// for removing warnings when Breeze does not find native libraries
-//
-// javaOptions in ThisBuild ++= Seq("-Dcom.github.fommil.netlib.BLAS=com.github.fommil.netlib.F2jBLAS",
-//   "-Dcom.github.fommil.netlib.LAPACK=com.github.fommil.netlib.F2jLAPACK",
-//   "-Dcom.github.fommil.netlib.ARPACK=com.github.fommil.netlib.F2jARPACK")
+EclipseKeys.eclipseOutput := Some("target.eclipse")
 
-// Metadata
+//*** Metadata for the build
 
 name in ThisBuild := "Jandom"
 
@@ -64,20 +77,20 @@ homepage in ThisBuild := Some(url("https://github.com/jandom-devel/Jandom"))
 
 startYear in ThisBuild := Some(2011)
 
-developers := List(
-  new Developer(
+developers in ThisBuild := List(
+  Developer(
     "amato",
     "Gianluca Amato", "gianluca.amato@unich.it",
     url("http://www.sci.unich.it/~amato/")
   ),
-  new Developer(
+  Developer(
     "scozzari",
     "Francesca Scozzari", "francesca.scozzari@unich.it",
     url("http://www.sci.unich.it/~scozzari/")
   )
 )
 
-scmInfo := Some(new ScmInfo(
+scmInfo in ThisBuild := Some(ScmInfo(
   url("https://github.com/jandom-devel/Jandom"),
   "scm:git:https://github.com/jandom-devel/Jandom.git",
   Some("scm:git:https://github.com/jandom-devel/Jandom.git")

core/build.sbt

@@ -1,53 +1,39 @@
+import CustomKeys._
+
 //*** Libraries
 
 libraryDependencies ++= Seq(
-  "org.apache.commons" % "commons-lang3" % "3.5",
-  "org.scalatest" %% "scalatest" % "3.0.0" % "test",
-  "org.scalacheck" %% "scalacheck" % "1.13.3" % "test",
-  "org.mockito" % "mockito-core" % "2.2.9" % "test",
-  "org.spire-math" %% "spire" % "0.12.0",
-  "org.scalanlp" %% "breeze" % "0.12",
-  "it.unich.scalafix" %% "scalafix" % "0.5.0",
-  // for using native linear algebra libraries
-  // "org.scalanlp" %% "breeze-natives" % "0.12",
-  "org.rogach" %% "scallop" % "2.0.3",
-  "org.scala-lang.modules" %% "scala-swing" % "1.0.2",
-  "org.scala-lang.modules" %% "scala-parser-combinators" % "1.0.4",
+  "org.apache.commons" % "commons-lang3" % "3.6",
+  "org.scalatest" %% "scalatest" % "3.0.4" % Test,
+  "org.scalacheck" %% "scalacheck" % "1.13.5" % Test,
+  "org.mockito" % "mockito-core" % "2.10.0" % Test,
+  "org.typelevel" %% "spire" % "0.14.1",
+  "it.unich.scalafix" %% "scalafix" % "0.7.0-SNAPSHOT",
+  "org.rogach" %% "scallop" % "3.1.0",
+  "org.scala-lang.modules" %% "scala-swing" % "2.0.0",
+  "org.scala-lang.modules" %% "scala-parser-combinators" % "1.0.6",
   "org.scala-lang" % "scala-reflect" % scalaVersion.value,
   // ASM is included in the Soot Jar
-  "soot" % "soot" % "2.5.0+git2" from "http://soot-build.cs.uni-paderborn.de/nightly/soot/soot-trunk.jar"
+  "ca.mcgill.sable" % "soot" %"3.0.0-SNAPSHOT"
 )
 
 //*** Additional source directories for PPL
 
-unmanagedJars in Compile ++= (pplJar.value map file).toSeq
-
 unmanagedSourceDirectories in Compile ++= (pplJar.value map { _ => (sourceDirectory in Compile).value / "ppl" }).toSeq
 
 unmanagedSourceDirectories in Test ++= (pplJar.value map { _ => (sourceDirectory in Test).value / "ppl" }).toSeq
 
-//*** Eclipse plugin
-
-EclipseKeys.createSrc := EclipseCreateSrc.Default +  EclipseCreateSrc.Managed
-
-EclipseKeys.executionEnvironment := Some(EclipseExecutionEnvironment.JavaSE17)
-
-EclipseKeys.eclipseOutput := Some("target.eclipse")
-
-// It would be nice to be able to exclude resource directories from compilation.
-
-managedSourceDirectories in Test := Seq()
+unmanagedJars in Compile ++= (pplJar.value map file).toSeq
 
-managedResourceDirectories in Test := Seq()
+//*** BuildInfo plugin
 
-managedResourceDirectories in Compile := Seq()
+buildInfoKeys ++= Seq[BuildInfoKey](name, version, scalaVersion, sbtVersion, gitHeadCommitSHA)
 
-unmanagedResourceDirectories in Compile := Seq()
+buildInfoPackage := "it.unich.jandom"
 
-//*** BuildInfo plugin
+//*** IDEA plugin
 
-gitHeadCommitSHA := Process("git rev-parse HEAD").lines.head
+ideOutputDirectory in Compile := Some(file("core/target/idea/classes"))
 
-buildInfoKeys := Seq[BuildInfoKey](name, version, scalaVersion, sbtVersion, gitHeadCommitSHA)
+ideOutputDirectory in Test := Some(file("core/target/idea/test-classes"))
 
-buildInfoPackage := "it.unich.jandom"

core/examples/Java/Congruence.java

@@ -1,8 +1,23 @@
 /**
+ * Copyright 2017 Mirko Bez, Stefano Munari, Sebastiano Valle
+ *
+ * This file is part of JANDOM: JVM-based Analyzer for Numerical DOMains
+ * JANDOM is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * JANDOM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of a
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with JANDOM.  If not, see <http://www.gnu.org/licenses/>.
  */
 
 class Congruence {
-	static void test() {
+	static void basic_congruence_add() {
 		int x = 3;
 		int y = 12;
 		if(x < 12)
@@ -11,7 +26,7 @@ static void test() {
 			x += 2;
 	}
 
-	static void testCongruence() {
+	static void basic_congruence_mul() {
 		int x = 2;
 		int y = 3;
 		int z = x*y;
@@ -20,6 +35,12 @@ static void testCongruence() {
 		}
 	}
 
+	/**
+	 * Example taken from
+	 * <a href="https://www-apr.lip6.fr/~mine/enseignement/mpri/attic/2013-2014/03b-num-nonrel_ok.pdf">
+	 * this slides of Minè (91/103)
+	 * </a>
+	 */
 	static void mineCongruence() {
 		int x = 0;
 		int y = 2;
@@ -32,6 +53,12 @@ static void mineCongruence() {
 		}
 	}
 
+	/**
+	 * Example taken from
+	 * <a href="https://www-apr.lip6.fr/~mine/enseignement/mpri/attic/2013-2014/03b-num-nonrel_ok.pdf">
+	 * this slides of Minè (96/103)
+	 * </a>
+	 */
 	static void mineProductIntervalCongruence() {
 		int x = 1;
 		while(x-10 <= 0) {

core/examples/Java/NumericalTestExtra.java

@@ -0,0 +1,58 @@
+/**
+ * Copyright 2017 Mirko Bez, Stefano Munari, Sebastiano Valle
+ *
+ * This file is part of JANDOM: JVM-based Analyzer for Numerical DOMains
+ * JANDOM is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * JANDOM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of a
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with JANDOM.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+public class NumericalTestExtra {
+
+    static void simple_multiplication_test() {
+		int a = 10;
+		int b = -2;
+		int c = 10 + a*b;
+    }
+    static void simple_algebra_example() {
+    	int a = 10;
+    	a = -a;
+    	int c = -100 * + a;
+    }
+
+    static void simple_loop_with_exit() {
+        int a = 0;
+        while(a <= 0)
+            a = 1;
+    }
+
+    static void remainder_of_one() {
+        int x = 1;
+        x = x % 2;
+    }
+
+    @SuppressWarnings("ALL")
+    static void filter() {
+    	int a = 2;
+    	a += -12;
+    	if(a < 0)
+    		a++;
+    	else
+    		a--;
+    }
+
+    static void divison_by_zero() {
+    	int x = 0;
+    	int y = 2;
+    	int z = y / x;
+    }
+}

core/examples/Java/SvBenchmark.java

@@ -0,0 +1,52 @@
+/**
+ * Copyright 2017 Mirko Bez, Stefano Munari, Sebastiano Valle
+ *
+ * This file is part of JANDOM: JVM-based Analyzer for Numerical DOMains
+ * JANDOM is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * JANDOM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of a
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with JANDOM.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+/**
+ * These examples are a Java-Translation of some C examples taken from the the
+ * <a href="https://github.com/sosy-lab/sv-benchmarks">sv-benchmark</a>
+ */
+public class SvBenchmark {
+    // taken from sv-benchmarks repository
+    static void sum04_false_unreach_call_true_termination(){
+        int i = 1;
+        int sn = 0;
+        while(i <= 8) {
+            if (i < 4)
+                sn = sn + (2);
+            i = i + 1;
+        }
+        // POST CONDITION: sn == 6
+    }
+
+    static void for_infinite_loop_2_true_unreach_call_false_termination() {
+        int i_U = 0;
+        int x = 0;
+        int y = 0;
+        int n = x*y*i_U + 12*3*x*y;
+        if(!(n > 0)) {
+            return;
+        }
+        boolean z = true;
+        for(i_U = 0; z; i_U++) {
+            x++;
+            //verifierAssert(!x ? 1 : 0);
+        }
+        //UNREACHABLE CODE
+        x += 12;
+    }
+}