From c05a241a05998500d19446d2be7bfeab5f5d5543 Mon Sep 17 00:00:00 2001
From: schillic <schillic@informatik.uni-freiburg.de>
Date: Sat, 1 Jul 2017 14:08:05 +0200
Subject: [PATCH] #182 - examples

---
 .../toy/diamondCallEmpty.bpl                  | 20 +++++++++++++
 .../toy/diamondCallError.bpl                  | 19 ++++++++++++
 .../toy/diamondCallErrorUselessCond.bpl       | 21 +++++++++++++
 .../toy/diamondCallGlobal.bpl                 | 30 +++++++++++++++++++
 .../toy/diamondDifferent.bpl                  | 20 +++++++++++++
 .../toy/errorLocalization/toy/diamondSame.bpl | 20 +++++++++++++
 .../toy/errorLocalization/toy/emptyCall.bpl   | 18 +++++++++++
 .../errorLocalization/toy/emptyProgram.bpl    | 13 ++++++++
 .../toy/errorLocalization/toy/loopNondet1.bpl | 13 ++++++++
 .../toy/errorLocalization/toy/loopNondet2.bpl | 14 +++++++++
 .../toy/errorLocalization/toy/loopNondet3.bpl | 14 +++++++++
 .../toy/errorLocalization/toy/loopNondet4.bpl | 14 +++++++++
 .../toy/errorLocalization/toy/loopNondet5.bpl | 14 +++++++++
 .../toy/loopNondetInitVal.bpl                 | 14 +++++++++
 .../toy/loopSeveralExits.bpl                  | 26 ++++++++++++++++
 15 files changed, 270 insertions(+)
 create mode 100644 trunk/examples/programs/toy/errorLocalization/toy/diamondCallEmpty.bpl
 create mode 100755 trunk/examples/programs/toy/errorLocalization/toy/diamondCallError.bpl
 create mode 100755 trunk/examples/programs/toy/errorLocalization/toy/diamondCallErrorUselessCond.bpl
 create mode 100755 trunk/examples/programs/toy/errorLocalization/toy/diamondCallGlobal.bpl
 create mode 100644 trunk/examples/programs/toy/errorLocalization/toy/diamondDifferent.bpl
 create mode 100755 trunk/examples/programs/toy/errorLocalization/toy/diamondSame.bpl
 create mode 100755 trunk/examples/programs/toy/errorLocalization/toy/emptyCall.bpl
 create mode 100755 trunk/examples/programs/toy/errorLocalization/toy/emptyProgram.bpl
 create mode 100755 trunk/examples/programs/toy/errorLocalization/toy/loopNondet1.bpl
 create mode 100755 trunk/examples/programs/toy/errorLocalization/toy/loopNondet2.bpl
 create mode 100755 trunk/examples/programs/toy/errorLocalization/toy/loopNondet3.bpl
 create mode 100755 trunk/examples/programs/toy/errorLocalization/toy/loopNondet4.bpl
 create mode 100755 trunk/examples/programs/toy/errorLocalization/toy/loopNondet5.bpl
 create mode 100755 trunk/examples/programs/toy/errorLocalization/toy/loopNondetInitVal.bpl
 create mode 100755 trunk/examples/programs/toy/errorLocalization/toy/loopSeveralExits.bpl

diff --git a/trunk/examples/programs/toy/errorLocalization/toy/diamondCallEmpty.bpl b/trunk/examples/programs/toy/errorLocalization/toy/diamondCallEmpty.bpl
new file mode 100644
index 00000000000..b2fa07989f9
--- /dev/null
+++ b/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 ()
+{
+}
diff --git a/trunk/examples/programs/toy/errorLocalization/toy/diamondCallError.bpl b/trunk/examples/programs/toy/errorLocalization/toy/diamondCallError.bpl
new file mode 100755
index 00000000000..c3769ca3d78
--- /dev/null
+++ b/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;
+}
\ No newline at end of file
diff --git a/trunk/examples/programs/toy/errorLocalization/toy/diamondCallErrorUselessCond.bpl b/trunk/examples/programs/toy/errorLocalization/toy/diamondCallErrorUselessCond.bpl
new file mode 100755
index 00000000000..c81e2341d70
--- /dev/null
+++ b/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;
+}
\ No newline at end of file
diff --git a/trunk/examples/programs/toy/errorLocalization/toy/diamondCallGlobal.bpl b/trunk/examples/programs/toy/errorLocalization/toy/diamondCallGlobal.bpl
new file mode 100755
index 00000000000..c91c31f2ee8
--- /dev/null
+++ b/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;
+}
\ No newline at end of file
diff --git a/trunk/examples/programs/toy/errorLocalization/toy/diamondDifferent.bpl b/trunk/examples/programs/toy/errorLocalization/toy/diamondDifferent.bpl
new file mode 100644
index 00000000000..47d1e530fba
--- /dev/null
+++ b/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);
+}
diff --git a/trunk/examples/programs/toy/errorLocalization/toy/diamondSame.bpl b/trunk/examples/programs/toy/errorLocalization/toy/diamondSame.bpl
new file mode 100755
index 00000000000..b260d29886a
--- /dev/null
+++ b/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 ;
\ No newline at end of file
diff --git a/trunk/examples/programs/toy/errorLocalization/toy/emptyCall.bpl b/trunk/examples/programs/toy/errorLocalization/toy/emptyCall.bpl
new file mode 100755
index 00000000000..9836dbc7d74
--- /dev/null
+++ b/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 ;
\ No newline at end of file
diff --git a/trunk/examples/programs/toy/errorLocalization/toy/emptyProgram.bpl b/trunk/examples/programs/toy/errorLocalization/toy/emptyProgram.bpl
new file mode 100755
index 00000000000..3dc964a46b7
--- /dev/null
+++ b/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 ;
\ No newline at end of file
diff --git a/trunk/examples/programs/toy/errorLocalization/toy/loopNondet1.bpl b/trunk/examples/programs/toy/errorLocalization/toy/loopNondet1.bpl
new file mode 100755
index 00000000000..5e1c3725c11
--- /dev/null
+++ b/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);
+}
\ No newline at end of file
diff --git a/trunk/examples/programs/toy/errorLocalization/toy/loopNondet2.bpl b/trunk/examples/programs/toy/errorLocalization/toy/loopNondet2.bpl
new file mode 100755
index 00000000000..b540ebdbd6b
--- /dev/null
+++ b/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);
+}
\ No newline at end of file
diff --git a/trunk/examples/programs/toy/errorLocalization/toy/loopNondet3.bpl b/trunk/examples/programs/toy/errorLocalization/toy/loopNondet3.bpl
new file mode 100755
index 00000000000..1d37bfa80aa
--- /dev/null
+++ b/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);
+}
\ No newline at end of file
diff --git a/trunk/examples/programs/toy/errorLocalization/toy/loopNondet4.bpl b/trunk/examples/programs/toy/errorLocalization/toy/loopNondet4.bpl
new file mode 100755
index 00000000000..6a029f0ff90
--- /dev/null
+++ b/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);
+}
\ No newline at end of file
diff --git a/trunk/examples/programs/toy/errorLocalization/toy/loopNondet5.bpl b/trunk/examples/programs/toy/errorLocalization/toy/loopNondet5.bpl
new file mode 100755
index 00000000000..f3c40569e82
--- /dev/null
+++ b/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);
+}
\ No newline at end of file
diff --git a/trunk/examples/programs/toy/errorLocalization/toy/loopNondetInitVal.bpl b/trunk/examples/programs/toy/errorLocalization/toy/loopNondetInitVal.bpl
new file mode 100755
index 00000000000..5570b8ec186
--- /dev/null
+++ b/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);
+}
\ No newline at end of file
diff --git a/trunk/examples/programs/toy/errorLocalization/toy/loopSeveralExits.bpl b/trunk/examples/programs/toy/errorLocalization/toy/loopSeveralExits.bpl
new file mode 100755
index 00000000000..86cae4d9fc6
--- /dev/null
+++ b/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);
+}