#182 - examples

trunk/examples/programs/toy/errorLocalization/toy/diamondCallEmpty.bpl

@@ -0,0 +1,20 @@
+//#Unsafe
+/*
+ * Author: Christian Schilling (schillic@informatik.uni-freiburg.de)
+ * Date: 2017-06-07
+ */
+
+procedure main() {
+	var x: int;
+	if (x > 0) {
+		call callee();
+	} else {
+		call callee();
+	}
+	assert(false);
+}
+
+
+procedure callee() returns ()
+{
+}

trunk/examples/programs/toy/errorLocalization/toy/diamondCallError.bpl

@@ -0,0 +1,19 @@
+//#Unsafe
+/*
+ * Author: Christian Schilling (schillic@informatik.uni-freiburg.de)
+ * Date: 2017-06-19
+ */
+
+procedure main() {
+  var x: int;
+
+  if (x > 2) {
+    call foo();
+  } else {
+    call foo();
+  }
+}
+
+procedure foo() returns () {
+    assert false;
+}

trunk/examples/programs/toy/errorLocalization/toy/diamondCallErrorUselessCond.bpl

@@ -0,0 +1,21 @@
+//#Unsafe
+/*
+ * Author: Christian Schilling (schillic@informatik.uni-freiburg.de)
+ * Date: 2017-06-19
+ */
+
+procedure main() {
+  var x: int;
+
+  if (true) {
+  }
+  if (x > 2) {
+    call foo();
+  } else {
+    call foo();
+  }
+}
+
+procedure foo() returns () {
+    assert false;
+}

trunk/examples/programs/toy/errorLocalization/toy/diamondCallGlobal.bpl

@@ -0,0 +1,30 @@
+//#Unsafe
+/*
+ * Author: Christian Schilling (schillic@informatik.uni-freiburg.de)
+ * Date: 2017-06-19
+ */
+
+var g: int;
+
+procedure main() returns ();
+modifies g;
+
+implementation main() {
+  var x: int;
+
+  g := 0;
+  if (x > 2) {
+    call foo();
+  }
+  if (x <= 2) {
+    call foo();
+  }
+  assert(g == 0);
+}
+
+procedure foo() returns ();
+modifies g;
+
+implementation foo() returns () {
+    g := 1;
+}

trunk/examples/programs/toy/errorLocalization/toy/diamondDifferent.bpl

@@ -0,0 +1,20 @@
+//#Unsafe
+/*
+ * Author: Christian Schilling (schillic@informatik.uni-freiburg.de)
+ * Date: 2017-06-02
+ */
+
+
+procedure main()
+{
+  var x, y: int;
+
+  y := 1;
+  havoc x;
+  if (x > 0) {
+    y := 0;
+  } else {
+    x := 0;
+  }
+  assert(y == 1);
+}

trunk/examples/programs/toy/errorLocalization/toy/diamondSame.bpl

@@ -0,0 +1,20 @@
+//#Unsafe
+/*
+ * Author: Christian Schilling (schillic@informatik.uni-freiburg.de)
+ * Date: 2017-06-30
+ */
+
+implementation main() returns () {
+    var x: int;
+
+    if (x > 0) {
+        x := 0;
+    } else {
+        x := 0;
+    }
+    assert false;
+}
+
+procedure main() returns ();
+modifies ;
+modifies ;

trunk/examples/programs/toy/errorLocalization/toy/emptyCall.bpl

@@ -0,0 +1,18 @@
+//#Unsafe
+/*
+ * Author: Christian Schilling (schillic@informatik.uni-freiburg.de)
+ * Date: 2017-06-14
+ */
+
+implementation main() returns (){
+    call init();
+    assert false;
+}
+
+implementation init() returns (){
+}
+
+procedure main() returns ();
+modifies ;
+procedure init() returns ();
+modifies ;

trunk/examples/programs/toy/errorLocalization/toy/emptyProgram.bpl

@@ -0,0 +1,13 @@
+//#Unsafe
+/*
+ * Author: Christian Schilling (schillic@informatik.uni-freiburg.de)
+ * Date: 2017-06-12
+ */
+
+implementation main() returns (){
+    assert false;
+}
+
+procedure main() returns ();
+modifies ;
+modifies ;

trunk/examples/programs/toy/errorLocalization/toy/loopNondet1.bpl

@@ -0,0 +1,13 @@
+//#Unsafe
+/*
+ * Author: Christian Schilling (schillic@informatik.uni-freiburg.de)
+ * Date: 2017-06-25
+ */
+
+procedure main() returns () {
+  var x: int;
+
+  while (*) {
+  }
+  assert(x == 0);
+}

trunk/examples/programs/toy/errorLocalization/toy/loopNondet2.bpl

@@ -0,0 +1,14 @@
+//#Unsafe
+/*
+ * Author: Christian Schilling (schillic@informatik.uni-freiburg.de)
+ * Date: 2017-06-25
+ */
+
+procedure main() returns () {
+  var x: int;
+
+  while (*) {
+    x := 1;
+  }
+  assert(x == 0);
+}

trunk/examples/programs/toy/errorLocalization/toy/loopNondet3.bpl

@@ -0,0 +1,14 @@
+//#Unsafe
+/*
+ * Author: Christian Schilling (schillic@informatik.uni-freiburg.de)
+ * Date: 2017-06-25
+ */
+
+procedure main() returns () {
+  var x: int;
+
+  while (*) {
+    x := 0;
+  }
+  assert(x == 0);
+}

trunk/examples/programs/toy/errorLocalization/toy/loopNondet4.bpl

@@ -0,0 +1,14 @@
+//#Unsafe
+/*
+ * Author: Christian Schilling (schillic@informatik.uni-freiburg.de)
+ * Date: 2017-06-25
+ */
+
+procedure main() returns () {
+  var x: int;
+
+  while (*) {
+    x := x + 1;
+  }
+  assert(x == 0);
+}

trunk/examples/programs/toy/errorLocalization/toy/loopNondet5.bpl

@@ -0,0 +1,14 @@
+//#Unsafe
+/*
+ * Author: Christian Schilling (schillic@informatik.uni-freiburg.de)
+ * Date: 2017-06-25
+ */
+
+procedure main() returns () {
+  var x: int;
+
+  while (*) {
+    havoc x;
+  }
+  assert(x == 0);
+}

trunk/examples/programs/toy/errorLocalization/toy/loopNondetInitVal.bpl

@@ -0,0 +1,14 @@
+//#Unsafe
+/*
+ * Author: Christian Schilling (schillic@informatik.uni-freiburg.de)
+ * Date: 2017-06-20
+ */
+
+procedure main() {
+  var x,y: int;
+
+  while (x > 0) {
+    x := x - 1;
+  }
+  assert(y == 0);
+}

trunk/examples/programs/toy/errorLocalization/toy/loopSeveralExits.bpl

@@ -0,0 +1,26 @@
+//#Unsafe
+/*
+ * Author: Christian Schilling (schillic@informatik.uni-freiburg.de)
+ * Date: 2017-06-28
+ */
+
+procedure main() {
+  var x: int;
+
+  while (x >= 0) {
+    x := x - 1;
+    if (x == 1) {
+      break;
+    }
+    if (x == 4) {
+      break;
+    }
+    if (x == 7) {
+      break;
+    }
+    if (x == 10) {
+      break;
+    }
+  }
+  assert(x == 0);
+}