Merge pull request #21 from mina1604/master

examples for cade

examples/arrays/absolute_prop1.spec

@@ -1,12 +1,11 @@
 func main()
 {
 	Int[] a;
-	Int[] b;
+	const Int[] b;
 
-	Int i;
-	Int blength;
+	const Int blength;
 
-	i = 0;
+	Int i = 0;
 	while(i < blength)
 	{
 		if(b[i] >= 0)
@@ -26,12 +25,12 @@ func main()
 		(=>
 			(and
 				(<= 0 k)
-				(< k (blength main_end))
+				(< k blength)
 			)
 			(or
 				(= (a main_end k) (b main_end k) )
 				(= (a main_end k) (- (b main_end k)) )
 			)
 		)
 	)
-)
+)

examples/arrays/absolute_prop2.spec

@@ -0,0 +1,33 @@
+func main()
+{
+	Int[] a;
+	const Int[] b;
+
+	const Int blength;
+
+	Int i = 0;
+	while(i < blength)
+	{
+		if(b[i] >= 0)
+		{
+			a[i] = b[i];
+		}
+		else
+		{
+			a[i] = -b[i];
+		}
+		i = i + 1;
+	}
+}
+
+(assert-not
+	(forall ((k Int))
+		(=>
+			(and
+				(<= 0 k)
+				(< k blength)
+			)
+				(<= 0 (a main_end k))
+		)
+	)
+)

examples/arrays/atleast_one_iteration.spec

@@ -0,0 +1,21 @@
+func main()
+{
+  const Int[] a;
+  const Int alength;
+
+  Int i = 0;
+  Int j = 0;
+  while(i < alength)
+  {
+    i = i + 1;
+    j = 1;
+  }
+}
+
+
+(assert-not
+  (=>
+    (< 0 alength)
+    (= (j main_end) 1)
+  )
+)

examples/arrays/both_or_none.spec

@@ -0,0 +1,48 @@
+// for each position p: if a[p] is 1, set b[p] to 1, otherwise set it to zero.
+// Prove that either both a[p] is 1 and b[p] is 1, or both a[p] is not 1 and b[p] is zero
+// similar to https://github.com/sosy-lab/sv-benchmarks/blob/master/c/array-examples/standard_running_true-unreach-call.c
+// but simplified
+
+func main()
+{
+  const Int[] a;
+  const Int alength;
+  Int[] b;
+
+  Int i = 0;
+  while(i < alength)
+  {
+    if (a[i] == 1)
+    {
+      b[i] = 1;
+    }
+    else
+    {
+      b[i] = 0;
+    }
+    i = i + 1;
+  }
+}
+
+
+(assert-not
+  (forall ((j Int))
+    (=>
+      (and
+        (<= 0 j)
+        (< j alength)
+        (<= 0 alength)
+      )
+      (or
+        (and
+          (= (a j) 1)
+          (= (b main_end j) 1)
+        )
+        (and
+          (not (= (a j) 1) )
+          (= (b main_end j) 0)
+        )
+      )
+    )
+  )
+)

examples/arrays/check_equal_set_flag.spec

@@ -0,0 +1,43 @@
+// check whether two arrays are the same at each position. If not, set the flag r to 1.
+// Prove that if flag was not set to 1, then arrays are equal.
+// similar to all of the following examples:
+// https://github.com/sosy-lab/sv-benchmarks/blob/master/c/array-examples/standard_compare_true-unreach-call_ground.c
+// https://github.com/sosy-lab/sv-benchmarks/blob/master/c/array-examples/standard_strcmp_true-unreach-call_ground.c
+// https://github.com/sosy-lab/sv-benchmarks/blob/master/c/array-examples/standard_password_true-unreach-call_ground.c
+
+func main()
+{
+  const Int[] a;
+  const Int[] b;
+  const Int length;
+
+  Int r;
+  Int i = 0;
+  while(i < length)
+  {
+    if(a[i] != b[i])
+    {
+      r = 1;
+    }
+    else
+    {
+      skip;
+    }
+    i = i + 1;
+  }
+}
+
+(assert-not
+  (forall ((k Int))
+    (=>
+      (and
+        (<= 0 k)
+        (< k length)
+        (<= 0 length)
+        (not (= (r (l16 zero)) 1))
+        (not (= (r main_end) 1))
+      )
+      (= (a k)(b k))
+    )
+  )
+)

examples/arrays/copy.spec

@@ -0,0 +1,27 @@
+func main()
+{
+	Int[] a;
+	const Int[] b;
+	Int i;
+	const Int blength;
+
+	i = 0;
+	while(i < blength)
+	{
+		a[i] = b[i];
+		i = i + 1;
+	}
+}
+
+(assert-not
+	(forall ((j Int))
+		(=>
+			(and
+				(<= 0 blength)
+				(<= 0 j)
+				(< j blength)
+			)
+			(= (a main_end j) (b j))
+		)
+	)
+)

examples/arrays/copy_nonzero_prop1.spec

@@ -0,0 +1,36 @@
+func main()
+{
+	Int[] a;
+
+	const Int[] b;
+	const Int blength;
+
+	Int i = 0;
+	Int alength = 0;
+	while(i < blength)
+	{
+		if (b[i] != 0)
+		{
+			a[alength] = b[i];
+			alength = alength + 1;
+		}
+		else
+		{
+			skip;
+		}
+		i = i + 1;
+	}
+}
+
+(assert-not
+	(forall ((k Int))
+		(=>
+			(and
+				(<= 0 blength)
+				(<= 0 k)
+				(< k (alength main_end))
+			)
+			(not (= (a main_end k) 0))
+		)
+	)
+)

examples/arrays/copy_nonzero_prop2.spec

@@ -0,0 +1,36 @@
+func main()
+{
+	Int[] a;
+	const Int[] b;
+	const Int blength;
+
+	 Inti = 0;
+	Int alength = 0;
+	while(i < blength)
+	{
+		if (b[i] != 0)
+		{
+			a[alength] = b[i];
+			alength = alength + 1;
+		} else
+		{
+			skip;
+		}
+		i = i + 1;
+	}
+}
+
+(assert-not
+	(forall ((k Int))
+		(exists ((l Int))
+			(=>
+				(and
+					(<= 0 k)
+					(<= 0 blength)
+					(< k (alength main_end))
+				)
+				(= (a main_end k) (b l))
+			)
+		)
+	)
+)

examples/arrays/copy_odd.spec

@@ -0,0 +1,26 @@
+func main()
+{
+	Int[] a;
+	const Int[] b;
+	const Int blength;
+
+	Int i = 0;
+	while (i < (blength / 2))
+	{
+		a[i] = b[i*2];
+		i = i + 1;
+	}
+}
+
+(assert-not
+	(forall ((k Int))
+		(=>
+			(and
+				(<= 0 k)
+				(< k (/ blength 2) )
+				(<= 0 blength)
+			)
+			(= (a main_end k) (b main_end (* k 2)))
+		)
+	)
+)

examples/arrays/copy_partial.spec

@@ -1,25 +1,11 @@
-//int [] a, b;
-//int i, blength, k;
-//
-//requires 0 <= blength;
-//
-//requires k <= blength;
-//requires i == 0;
-//ensures forall int j, 0 <= j & j < k ==> a[j] == b[j];
-//
-//while (i < k) do
-//:: true -> a[i] = b[i]; i = i + 1;
-//od
-
 func main()
 {
 	Int[] a;
-	Int[] b;
-	Int i;
-	Int blength;
-	Int k;
+	const Int[] b;
+	const Int blength;
+	const Int k;
 
-	i = 0;
+	Int i = 0;
 	while(i < k)
 	{
 		a[i] = b[i];
@@ -29,15 +15,15 @@ func main()
 
 (assert-not
 	(=>
-		(<= (k main_end) (blength main_end))
+		(<= k blength)
 		(forall ((j Int))
 			(=>
 				(and
 					(<= 0 j)
-					(< j (k main_end))
+					(< j k)
 				)
-				(= (a main_end j) (b main_end j))
+				(= (a main_end j) (b j))
 			)
 		)
 	)
-)
+)

examples/arrays/copy_positive.spec

@@ -0,0 +1,34 @@
+func main()
+{
+	Int[] a;
+	const Int[] b;
+	const Int blength;
+
+	Int i = 0;
+	Int j = 0;
+	while(i < blength)
+	{
+		if (b[i] >= 0)
+		{
+			a[j] = b[i];
+			j = j + 1;
+		} else
+		{
+			skip;
+		}
+		i = i + 1;
+	}
+}
+
+(assert-not
+	(forall ((k Int))
+		(=>
+			(and
+				(<= 0 k)
+				(< k (j main_end))
+				(<= 0 blength)
+			)
+			(<= 0 (a main_end k))
+		)
+	)
+)