From 053d885d1c61eacadb463e8e4e76b0bc943c32c2 Mon Sep 17 00:00:00 2001
From: Guillaume Petiot <guillaume.petiot@cea.fr>
Date: Mon, 4 Mar 2013 13:55:14 +0000
Subject: [PATCH]
---
.../memory_model/experiments/fibonacci/fibo.c | 24 +-
.../experiments/get_sub/Replace.c | 215 ++++++++++++++++++
.../get_sub/test_parameters_getsub.pl | 36 +++
.../experiments/matmult/matmult.c | 8 +-
4 files changed, 279 insertions(+), 4 deletions(-)
create mode 100644 src/plugins/e-acsl/doc/memory_model/experiments/get_sub/Replace.c
create mode 100644 src/plugins/e-acsl/doc/memory_model/experiments/get_sub/test_parameters_getsub.pl
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/fibo.c b/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/fibo.c
index 7d841734de9..f730673e890 100644
--- a/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/fibo.c
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/fibo.c
@@ -1,5 +1,8 @@
+#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);
+}
+
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/Replace.c b/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/Replace.c
new file mode 100644
index 00000000000..d8eadf8c6d5
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/Replace.c
@@ -0,0 +1,215 @@
+/* -*- 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);
+ }
+}
+
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/test_parameters_getsub.pl b/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/test_parameters_getsub.pl
new file mode 100644
index 00000000000..52766e82aeb
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/test_parameters_getsub.pl
@@ -0,0 +1,36 @@
+:- 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).
+
+
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/matmult/matmult.c b/src/plugins/e-acsl/doc/memory_model/experiments/matmult/matmult.c
index bb1d9b389b7..d1639050780 100644
--- a/src/plugins/e-acsl/doc/memory_model/experiments/matmult/matmult.c
+++ b/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)
/*
--
GitLab