[e-acsl] + matmult example for experiments

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

+/* MDH WCET BENCHMARK SUITE. File version $Id: matmult.c,v 1.3 2005/11/11 10:31:26 ael01 Exp $ */
+
+/*----------------------------------------------------------------------*
+ * To make this program compile under our assumed embedded environment,
+ * we had to make several changes:
+ * - Declare all functions in ANSI style, not K&R.
+ *   this includes adding return types in all cases!
+ * - Declare function prototypes
+ * - Disable all output
+ * - Disable all UNIX-style includes
+ *
+ * This is a program that was developed from mm.c to matmult.c by
+ * Thomas Lundqvist at Chalmers.
+ *----------------------------------------------------------------------*/
+
+#define UPPERLIMIT 10
+
+void 
+Multiply(int ** A, int ** B, int ** Res)
+/*
+ * Multiplies arrays A and B and stores the result in ResultArray.
+ */
+{
+  register int    Outer, Inner, Index;
+
+  //@ ghost int old_Outer = -1; 
+  for (Outer = 0; Outer < UPPERLIMIT; Outer++) {
+    //@ assert old_Outer != Outer;
+    //@ ghost old_Outer = Outer;
+    //@ assert 0 <= Outer < 10;
+    //@ ghost int old_Inner = -1;
+    for (Inner = 0; Inner < UPPERLIMIT; Inner++) {
+      //@ assert old_Inner != Inner;
+      //@ ghost old_Inner = Inner;
+      //@ assert 0 <= Inner < 10;
+      Res[Outer][Inner] = 0;
+      //@ assert Res[Outer][Inner] == 0;
+      //@ ghost int old_Index = -1;
+      for (Index = 0; Index < UPPERLIMIT; Index++) {
+	//@ assert old_Index != Index;
+	//@ ghost old_Index = Index;
+	//@ assert 0 <= Index < 10;
+	//@ 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 Inner == 10;
+  }
+  //@ assert Outer == 10;
+}

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

+:- module(test_parameters).
+
+:- import create_input_val/3 from substitution.
+
+:- export dom/4.
+:- export create_input_vals/2.
+:- export unquantif_preconds/2.
+:- export quantif_preconds/2.
+:- 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',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),
+  true.
+
+unquantif_preconds('Multiply',[]).
+quantif_preconds('Multiply',[]).
+strategy('Multiply',[]).
+precondition_of(0,0).