Merge pull request #21 from rems-project/bugfix/missing-semicolons

Fix missing semicolons, make `check.sh` run on *.broken.c examples

check.sh

@@ -8,17 +8,24 @@ else
     CN=cn
 fi
 
-
 good=0
 bad=0
 
 for file in src/examples/*c;
 do
+    echo "Checking $file ..."
+    $CN $file 
+    retval=$?
     if [[ $file == *.broken.c ]]
     then
-        echo "(skipping $file)"
+        if [[ $retval -eq 1 ]]; 
+        then
+            good=$(($good+1))
+        else
+            bad=$(($bad+1))
+        fi
     else
-        if $CN $file
+        if [[ $retval -eq 0 ]]; 
         then
             good=$(($good+1))
         else
@@ -27,7 +34,6 @@ do
     fi
 done
 
-
 echo "----------------------------"
 echo "$good good, $bad bad"
 echo "----------------------------"

src/examples/array_load.broken.c

@@ -1,7 +1,7 @@
 int read (int *p, int n, int i)
 /*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) };
-             0i32 <= i && i < n
-    ensures take a2 = each(i32 j; 0i32 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) } @*/
+             0i32 <= i && i < n; 
+    ensures take a2 = each(i32 j; 0i32 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) }; @*/
 {
   return p[i];
 }

src/examples/list_rev_spec.h

@@ -1,4 +1,4 @@
-#include "list_snoc_spec"
+#include "list_snoc_spec.h"
 
 /*@
 function [rec] (datatype seq) rev(datatype seq xs) {

src/examples/read.broken.c

@@ -1,5 +1,5 @@
 int read (int *p)
-/*@ requires take v1 = Owned<int>(p) @*/
+/*@ requires take v1 = Owned<int>(p); @*/
 {
   return *p;
 }

src/examples/slf0_basic_incr.signed.broken.c

@@ -1,6 +1,6 @@
 void incr (int *p)
-/*@ requires take u = Block<int>(p)
-    ensures take v = Owned<int>(p) 
+/*@ requires take u = Block<int>(p); 
+    ensures take v = Owned<int>(p); 
 @*/
 {
   *p = *p+1;

src/examples/slf0_incr.broken.c

@@ -2,7 +2,7 @@ void incr (int *p)
 /* --BEGIN-- */
 /*@ requires take v1 = Block<int>(p);
     ensures take v2 = Owned<int>(p);
-            v2 == v1+1i32 @*/
+            v2 == v1+1i32; @*/
 /* --END-- */
 {
   int n = *p;

src/examples/slf14_basic_succ_using_incr_attempt.broken.c

@@ -3,7 +3,7 @@
 
 unsigned int succ_using_incr_attempt(unsigned int n)
 /* --BEGIN-- */
-/*@ ensures return == n+1u32
+/*@ ensures return == n+1u32; 
 @*/
 /* --END-- */
 {

src/examples/slf5_basic_aliased_call.broken.c

@@ -1,9 +1,9 @@
 #include "slf4_basic_incr_two.c"
 
 void aliased_call (unsigned int *p)
-/*@ requires take n1 = Owned(p)
+/*@ requires take n1 = Owned(p); 
     ensures take n2 = Owned(p);
-            n2 == n1 + 2u32 @*/
+            n2 == n1 + 2u32; @*/
 {
   incr_two(p, p);
 }

src/examples/transpose.broken.c

@@ -1,10 +1,10 @@
 struct point { int x; int y; };
 
 void transpose (struct point *p) 
-/*@ requires take s = Owned<struct point>(p)
-    ensures take s2 = Owned<struct point>(p);
+/*@ requires take s = Owned<struct point>(p); 
+    ensures take s2 = Owned<struct point>(p); 
             s2.x == s.y;
-            s2.y == s.x
+            s2.y == s.x; 
 @*/
 {
   int temp_x = p->x;