[e-acsl] article in progress

src/plugins/e-acsl/doc/memory_model/article.tex

@@ -703,6 +703,8 @@ $ptr$ are initialized, 0 otherwise.
     \hline
     $BubbleSort$ & 31 & 963s & 873 & 44 & 44 \\
     \hline
+    $MultiplyMatrix$ & 44 & 146s & 9 & 44 & 44 \\
+    \hline
   \end{tabular}
   \caption{Experimental results}
 \end{figure}~\\

src/plugins/e-acsl/doc/memory_model/experiments/matmult/matmult.c

@@ -13,10 +13,9 @@
  * Thomas Lundqvist at Chalmers.
  *----------------------------------------------------------------------*/
 
-#define UPPERLIMIT 10
 
 void 
-Multiply(int ** A, int ** B, int ** Res)
+Multiply(int ** A, int ** B, int ** Res, int n)
 /*
  * Multiplies arrays A and B and stores the result in ResultArray.
  */
@@ -24,29 +23,29 @@ Multiply(int ** A, int ** B, int ** Res)
   register int    Outer, Inner, Index;
 
   //@ ghost int old_Outer = -1; 
-  for (Outer = 0; Outer < UPPERLIMIT; Outer++) {
+  for (Outer = 0; Outer < n; Outer++) {
     //@ assert old_Outer != Outer;
     //@ ghost old_Outer = Outer;
-    //@ assert 0 <= Outer < 10;
+    //@ assert 0 <= Outer < n;
     //@ ghost int old_Inner = -1;
-    for (Inner = 0; Inner < UPPERLIMIT; Inner++) {
+    for (Inner = 0; Inner < n; Inner++) {
       //@ assert old_Inner != Inner;
       //@ ghost old_Inner = Inner;
-      //@ assert 0 <= Inner < 10;
+      //@ assert 0 <= Inner < n;
       Res[Outer][Inner] = 0;
       //@ assert Res[Outer][Inner] == 0;
       //@ ghost int old_Index = -1;
-      for (Index = 0; Index < UPPERLIMIT; Index++) {
+      for (Index = 0; Index < n; Index++) {
 	//@ assert old_Index != Index;
 	//@ ghost old_Index = Index;
-	//@ assert 0 <= Index < 10;
+	//@ assert 0 <= Index < n;
 	//@ ghost int res = Res[Outer][Inner];
 	Res[Outer][Inner] += A[Outer][Index] * B[Index][Inner];
 	//@ assert Res[Outer][Inner] == res + A[Outer][Index] * B[Index][Inner];
       }
-      //@ assert Index == 10;
+      //@ assert Index == n;
     }
-    //@ assert Inner == 10;
+    //@ assert Inner == n;
   }
-  //@ assert Outer == 10;
+  //@ assert Outer == n;
 }

src/plugins/e-acsl/doc/memory_model/experiments/matmult/test_parameters.pl

@@ -9,20 +9,32 @@
 :- export strategy/2.
 :- export precondition_of/2.
 
-dom('Multiply',dim(cont('A',_)),[],int([10])).
-dom('Multiply',dim(cont('B',_)),[],int([10])).
-dom('Multiply',dim(cont('Res',_)),[],int([10])).
+dom('Multiply',dim(cont('A',_)),[],int([0..100])).
+dom('Multiply',dim(cont('B',_)),[],int([0..100])).
+dom('Multiply',dim(cont('Res',_)),[],int([0..100])).
 dom('Multiply',cont(cont('A',_),_),[],int([-100..100])).
 dom('Multiply',cont(cont('B',_),_),[],int([-100..100])).
 dom('Multiply',cont(cont('Res',_),_),[],int([0])).
 
 create_input_vals('Multiply',Ins):-
-  create_input_val(dim('A'),int([10]),Ins),
-  create_input_val(dim('B'),int([10]),Ins),
-  create_input_val(dim('Res'),int([10]),Ins),
+  create_input_val(dim('A'),int([0..100]),Ins),
+  create_input_val(dim('B'),int([0..100]),Ins),
+  create_input_val(dim('Res'),int([0..100]),Ins),
+  create_input_val('n',int([2..10]),Ins),
   true.
 
-unquantif_preconds('Multiply',[]).
-quantif_preconds('Multiply',[]).
+unquantif_preconds('Multiply',[
+  cond(egal,'n',dim('A'),pre),
+  cond(egal,'n',dim('B'),pre),
+  cond(egal,'n',dim('Res'),pre)
+]).
+quantif_preconds('Multiply',[
+  uq_cond([I],[cond(supegal,I,0,pre),cond(inf,I,'n',pre)],
+          egal,'n',dim(cont('A',I))),
+  uq_cond([I],[cond(supegal,I,0,pre),cond(inf,I,'n',pre)],
+          egal,'n',dim(cont('B',I))),
+  uq_cond([I],[cond(supegal,I,0,pre),cond(inf,I,'n',pre)],
+          egal,'n',dim(cont('Res',I)))
+]).
 strategy('Multiply',[]).
 precondition_of(0,0).