No commit message

No commit message

src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/fibo.c

 
+#include "stdlib.h"
+
 /*@ requires n >= 3;
+  @ requires \valid(t+(0..n-1));
   @ ensures t[0] == 1;
   @ ensures t[1] == 1;
   @ ensures \forall int i; 2 <= i < n ==> t[i-2] + t[i-1] == t[i];
@@ -7,10 +10,11 @@
 void fibo(int *t, int n) {
   int i;
   t[0] = t[1] = 1;
-  //@ assert t[0] == 1;
-  //@ assert t[1] == 1;
 
-  //@ assert n >= 3;
+  /*@ loop invariant \forall int k; 2 <= k < i ==> t[k] == t[k-1] + t[k-2];
+    @ loop assigns i, *(t+(2..n-1));
+    @ loop variant n-i;
+    @*/
   for(i = 2; i < n; ) {
     //@ assert 2 <= i < n;
     t[i] = t[i-1] + t[i-2];
@@ -21,3 +25,17 @@ void fibo(int *t, int n) {
   }
   //@ assert i >= n;
 }
+
+
+/*@ ensures \result >= x;
+  @ assigns \nothing;
+  @*/
+int unbounded_random(int x);
+
+void driver() {
+  int n = unbounded_random(3);
+  int * t = malloc(n * sizeof(int));
+  fibo(t, n);
+  free(t);
+}
+

src/plugins/e-acsl/doc/memory_model/experiments/get_sub/Replace.c

+/*  -*- Last-Edit:  Mon Dec  7 10:31:51 1992 by Tarak S. Goradia; -*- */
+
+
+
+# include <stdio.h>
+#include <stdlib.h>
+#include <ctype.h>
+
+typedef char	bool;
+# define false 0
+# define true  1
+/*# define NULL 0*/
+
+# define MAXSTR 100
+# define MAXPAT MAXSTR
+
+# define ENDSTR  '\0'
+# define ESCAPE  '@'
+# define CLOSURE '*'
+# define BOL     '%'
+# define EOL     '$'
+# define ANY     '?'
+# define CCL     '['
+# define CCLEND  ']'
+# define NEGATE  '^'
+# define NCCL    '!'
+# define LITCHAR 'c'
+# define DITTO   -1
+# define DASH    '-'
+
+# define TAB     9
+# define NEWLINE 10
+
+# define CLOSIZE 1
+
+typedef char	character;
+typedef char string[MAXSTR];
+
+
+
+
+/*@ requires \valid_read(j);
+  @ behavior b1:
+  @  assumes *j >= maxset;
+  @  assigns \nothing;
+  @  ensures \result == false;
+  @ behavior b2:
+  @  assumes *j < maxset;
+  @  requires \valid(outset+(0..maxset-1));
+  @  requires \valid(j);
+  @  assigns *j, outset[*j];
+  @  ensures j == \old(j)+1;
+  @  ensures outset[*j] == c;
+  @  ensures \result == true;
+  @ complete behaviors;
+  @ disjoint behaviors;
+  @*/
+int addstr(char c, char *outset, int *j, int maxset){
+  bool	result;
+  
+  /* b1 */
+  if (*j >= maxset){
+    result = false;
+  }
+  /* b2 */
+  else {
+    outset[*j] = c;  
+    *j = *j + 1;
+    result = true;
+  }
+  return result;
+}
+
+
+/*@ requires \valid_read(i);
+  @ requires \valid_read(s+(*i));
+  @ behavior b1:
+  @  assumes s[*i] != ESCAPE;
+  @  assigns \nothing;
+  @  ensures \result == s[*i];
+  @ behavior b2:
+  @  assumes s[*i] == ESCAPE;
+  @  assumes s[*i+1] == ENDSTR;
+  @  requires \valid_read(s+(*i+1));
+  @  assigns \nothing;
+  @  ensures \result == ESCAPE;
+  @ behavior b3:
+  @  assumes s[*i] == ESCAPE;
+  @  assumes s[*i+1] == 'n';
+  @  requires \valid_read(s+(*i+1));
+  @  assigns *i;
+  @  ensures \result == NEWLINE;
+  @ behavior b4:
+  @  assumes s[*i] == ESCAPE;
+  @  assumes s[*i+1] == 't';
+  @  requires \valid_read(s+(*i+1));
+  @  assigns *i;
+  @  ensures \result == TAB;
+  @ behavior b5:
+  @  assumes s[*i] == ESCAPE;
+  @  assumes s[*i+1] != ENDSTR;
+  @  assumes s[*i+1] != 'n';
+  @  assumes s[*i+1] != 't';
+  @  requires \valid_read(s+(*i+1));
+  @  assigns *i;
+  @  ensures \result == s[*i+1];
+  @ complete behaviors;
+  @ disjoint behaviors;
+  @*/
+char esc(char *s, int *i){
+  char	result;
+  
+  /* b1 */
+  if (s[*i] != ESCAPE){  
+    result = s[*i];
+  }
+  else{
+    /* b2 */
+    if(s[*i + 1] == ENDSTR){
+      result = ESCAPE;
+    }
+    else{
+      *i = *i + 1;
+      /* b3 */
+      if(s[*i] == 'n'){
+	result = NEWLINE;
+      }
+      else{
+	/* b4 */
+	if(s[*i] == 't'){
+	  result = TAB;
+	}
+	/* b5 */
+	else{
+	  result = s[*i];
+	}
+      }
+    }
+  }
+  return result;
+}
+
+
+/*@ requires \exists int i;
+  0 < i && arg[i] == ENDSTR && \valid_read(arg+(0..i-1));
+  @ requires \exists int i;
+  0 < i && sub[i] == ENDSTR && \valid(sub+(0..i-1));
+  @ behavior b2:
+  @  assumes \exists int i;
+  0 < i && sub[i] == ENDSTR && \valid(sub+(0..i-1)) && i >= MAXPAT;
+  @  ensures \result == 0;
+  @ behavior b3:
+  @  assumes \exists int i;
+  0 < i && sub[i] == ENDSTR && \valid(sub+(0..i-1)) && i < MAXPAT;
+  @  ensures \result >= 0;
+  @ complete behaviors;
+  @ disjoint behaviors;
+  @*/
+int makesub(char* arg, int from, character delim, char* sub){
+  int  result;
+  int	i, j;
+  bool	junk;
+  character	escjunk;
+  
+  j = 0;
+  i = from;
+
+  while ((arg[i] != delim) && (arg[i] != ENDSTR)) {
+    //@ assert arg[i] != delim;
+    //@ assert arg[i] != ENDSTR;
+    if ((arg[i] == (unsigned)('&'))){
+      junk = addstr(DITTO, sub, &j, MAXPAT);
+    }
+    else {
+      escjunk = esc(arg, &i);
+      junk = addstr(escjunk, sub, &j, MAXPAT);
+    }
+    
+    i = i + 1;
+  }
+  //@ assert arg[i] == delim || arg[i] == ENDSTR;
+  /* b1 */
+  if (arg[i] != delim){
+    // unreachable
+    result = 0;
+  }else {
+    //@ assert arg[i] == delim;
+    junk = addstr(ENDSTR, &(*sub), &j, MAXPAT);
+    /* b2 */
+    if (!junk){
+      result = 0;
+    }
+    /* b3 */
+    else{
+      result = i;
+    }
+  }
+  return result;
+}
+
+
+/*@ requires \exists int i; 0 < i && arg[i] == ENDSTR && \valid(arg+(0..i-1));
+  @ requires \exists int i; 0 < i && sub[i] == ENDSTR && \valid(sub+(0..i-1));
+  @*/
+bool getsub(char* arg, char* sub){
+  int	makeres;
+  makeres = makesub(arg, 0, ENDSTR, sub);
+  if(makeres > 0){
+    return(1);
+  }
+  else{
+    return(0);
+  }
+}
+

src/plugins/e-acsl/doc/memory_model/experiments/get_sub/test_parameters_getsub.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.
+
+:- export disable_label_history/1.
+disable_label_history(yes).
+dom('getsub',cont('arg__getsub',_),[],int([-128..127])).
+dom('getsub',cont('sub__getsub',_),[],int([-128..127])).
+% add new array domain e.g.:
+%  dom('yourFunName',cont('yourArray',_),[],int([min..max])).
+
+create_input_vals('getsub',Ins):-
+  create_input_val(dim('sub__getsub'),int([5..5]),Ins),
+  create_input_val(dim('arg__getsub'),int([7..7]),Ins),
+  true.
+% add new variable domain e.g.:
+%  create_input_val(yourVarName,int([min..max]),Ins), 
+
+
+unquantif_preconds('getsub',[cond(egal,cont('sub__getsub',4),0,pre),
+                             cond(egal,cont('arg__getsub',6),0,pre)]).
+
+quantif_preconds('getsub',[]).
+
+strategy('getsub',[]).
+
+precondition_of(0,0).
+
+

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

@@ -13,7 +13,13 @@
  * Thomas Lundqvist at Chalmers.
  *----------------------------------------------------------------------*/
 
-
+/*@ requires \valid(A+(0..n-1));
+  @ requires \valid(B+(0..n-1));
+  @ requires \valid(Res+(0..n-1));
+  @ requires \forall int i; 0 <= i < n ==> \valid(A[i]+(0..n-1));
+  @ requires \forall int i; 0 <= i < n ==> \valid(B[i]+(0..n-1));
+  @ requires \forall int i; 0 <= i < n ==> \valid(Res[i]+(0..n-1));
+  @*/
 void 
 Multiply(int ** A, int ** B, int ** Res, int n)
 /*