diff --git a/src/plugins/e-acsl/doc/memory_model/article.pdf b/src/plugins/e-acsl/doc/memory_model/article.pdf
index 68aba819e021eeb86b20d70db6d34042494b1538..9442066c1b36e315776d69c92986282a8635b8e5 100644
Binary files a/src/plugins/e-acsl/doc/memory_model/article.pdf and b/src/plugins/e-acsl/doc/memory_model/article.pdf differ
diff --git a/src/plugins/e-acsl/doc/memory_model/article.tex b/src/plugins/e-acsl/doc/memory_model/article.tex
index d6014bcecaee0c5344fce10a7062633e02af7fa6..4c206402d7ad9784da3010402606dcb78d6f8cf4 100644
--- a/src/plugins/e-acsl/doc/memory_model/article.tex
+++ b/src/plugins/e-acsl/doc/memory_model/article.tex
@@ -720,7 +720,7 @@ least one test case provoking a runtime error and this error has been found by
\hline
$Bsearch$ & 28 & 63s & 20 & 41 & 41 \\
\hline
- $Bsort$ & 37 & 273s & 153 & 45 & 47 \\
+ $Bsort$ & 37 & 273s & 153 & 47 & 45 \\
\hline
$Merge$ & 55 & 100s & 19 & 58 & 58 \\
\hline
@@ -728,6 +728,8 @@ least one test case provoking a runtime error and this error has been found by
\hline
$MultiplyMatrix$ & 44 & 146s & 9 & 44 & 44 \\
\hline
+ $get\_sub$ & 165 & 993s & 364 & 53 & 50 \\
+ \hline
\end{tabular}
\caption{Experimental results}
\label{fig:exp}
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
index d8eadf8c6d5ba9c7f3ac8aa585eac9ddf8cbfce9..df8c2cc629b02a3baa08750f0669c1f0f1bc3638 100644
--- 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
@@ -2,14 +2,16 @@
-# include <stdio.h>
-#include <stdlib.h>
+#include "stdio.h"
+#include "stdlib.h"
+
+/*
#include <ctype.h>
typedef char bool;
# define false 0
# define true 1
-/*# define NULL 0*/
+# define NULL 0
# define MAXSTR 100
# define MAXPAT MAXSTR
@@ -35,7 +37,7 @@ typedef char bool;
typedef char character;
typedef char string[MAXSTR];
-
+*/
@@ -43,30 +45,34 @@ typedef char string[MAXSTR];
@ behavior b1:
@ assumes *j >= maxset;
@ assigns \nothing;
- @ ensures \result == false;
+ @ ensures \result == 0;
@ behavior b2:
@ assumes *j < maxset;
- @ requires \valid(outset+(0..maxset-1));
@ requires \valid(j);
+ @ requires \valid(outset+(*j));
@ assigns *j, outset[*j];
- @ ensures j == \old(j)+1;
- @ ensures outset[*j] == c;
- @ ensures \result == true;
+ @ ensures *j == \old(*j)+1;
+ @ ensures outset[*j-1] == c;
+ @ ensures \result == 1;
@ complete behaviors;
@ disjoint behaviors;
@*/
int addstr(char c, char *outset, int *j, int maxset){
- bool result;
+ char result;
/* b1 */
if (*j >= maxset){
- result = false;
+ //@ assert *j >= maxset;
+ result = 0;
}
/* b2 */
else {
- outset[*j] = c;
+ //@ assert *j < maxset;
+ outset[*j] = c;
+ //@ ghost int tmp = *j;
*j = *j + 1;
- result = true;
+ //@ assert *j == tmp + 1;
+ result = 1;
}
return result;
}
@@ -75,35 +81,38 @@ int addstr(char c, char *outset, int *j, int maxset){
/*@ requires \valid_read(i);
@ requires \valid_read(s+(*i));
@ behavior b1:
- @ assumes s[*i] != ESCAPE;
+ @ assumes s[*i] != '@';
@ assigns \nothing;
@ ensures \result == s[*i];
@ behavior b2:
- @ assumes s[*i] == ESCAPE;
- @ assumes s[*i+1] == ENDSTR;
+ @ assumes s[*i] == '@';
+ @ assumes s[*i+1] == '\0';
@ requires \valid_read(s+(*i+1));
@ assigns \nothing;
- @ ensures \result == ESCAPE;
+ @ ensures \result == '@';
@ behavior b3:
- @ assumes s[*i] == ESCAPE;
+ @ assumes s[*i] == '@';
@ assumes s[*i+1] == 'n';
@ requires \valid_read(s+(*i+1));
@ assigns *i;
- @ ensures \result == NEWLINE;
+ @ ensures *i == \old(*i)+1;
+ @ ensures \result == 10;
@ behavior b4:
- @ assumes s[*i] == ESCAPE;
+ @ assumes s[*i] == '@';
@ assumes s[*i+1] == 't';
@ requires \valid_read(s+(*i+1));
@ assigns *i;
- @ ensures \result == TAB;
+ @ ensures *i == \old(*i)+1;
+ @ ensures \result == 9;
@ behavior b5:
- @ assumes s[*i] == ESCAPE;
- @ assumes s[*i+1] != ENDSTR;
+ @ assumes s[*i] == '@';
+ @ assumes s[*i+1] != '\0';
@ assumes s[*i+1] != 'n';
@ assumes s[*i+1] != 't';
@ requires \valid_read(s+(*i+1));
@ assigns *i;
- @ ensures \result == s[*i+1];
+ @ ensures *i == \old(*i)+1;
+ @ ensures \result == s[*i];
@ complete behaviors;
@ disjoint behaviors;
@*/
@@ -111,27 +120,37 @@ char esc(char *s, int *i){
char result;
/* b1 */
- if (s[*i] != ESCAPE){
+ if (s[*i] != '@'){
+ //@ assert s[*i] != '@';
result = s[*i];
}
else{
+ //@ assert s[*i] == '@';
/* b2 */
- if(s[*i + 1] == ENDSTR){
- result = ESCAPE;
+ if(s[*i + 1] == '\0'){
+ //@ assert s[*i+1] == '\0';
+ result = '@';
}
else{
+ //@ assert s[*i+1] != '\0';
+ //@ ghost int tmp = *i;
*i = *i + 1;
+ //@ assert *i == tmp + 1;
/* b3 */
if(s[*i] == 'n'){
- result = NEWLINE;
+ //@ assert s[*i] == 'n';
+ result = 10;
}
else{
+ //@ assert s[*i] != 'n';
/* b4 */
if(s[*i] == 't'){
- result = TAB;
+ //@ assert s[*i] == 't';
+ result = 9;
}
/* b5 */
else{
+ //@ assert s[*i] != 't';
result = s[*i];
}
}
@@ -141,57 +160,49 @@ char esc(char *s, int *i){
}
-/*@ 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 makesub(char* arg, int from, char delim, char* sub){
int result;
int i, j;
- bool junk;
- character escjunk;
+ char junk;
+ char escjunk;
j = 0;
i = from;
- while ((arg[i] != delim) && (arg[i] != ENDSTR)) {
+ while ((arg[i] != delim) && (arg[i] != '\0')) {
//@ assert arg[i] != delim;
- //@ assert arg[i] != ENDSTR;
+ //@ assert arg[i] != '\0';
if ((arg[i] == (unsigned)('&'))){
- junk = addstr(DITTO, sub, &j, MAXPAT);
+ //@ assert arg[i] == '&';
+ junk = addstr(-1, sub, &j, 100);
}
else {
+ //@ assert arg[i] != '&';
escjunk = esc(arg, &i);
- junk = addstr(escjunk, sub, &j, MAXPAT);
+ junk = addstr(escjunk, sub, &j, 100);
}
+ //@ ghost int tmp = i;
i = i + 1;
+ //@ assert i == tmp + 1;
}
- //@ assert arg[i] == delim || arg[i] == ENDSTR;
+ //@ assert arg[i] == delim || arg[i] == '\0';
/* b1 */
if (arg[i] != delim){
+ //@ assert arg[i] != delim;
// unreachable
result = 0;
}else {
//@ assert arg[i] == delim;
- junk = addstr(ENDSTR, &(*sub), &j, MAXPAT);
+ junk = addstr('\0', &(*sub), &j, 100);
/* b2 */
if (!junk){
+ //@ assert !junk;
result = 0;
}
/* b3 */
else{
+ //@ assert junk;
result = i;
}
}
@@ -199,17 +210,46 @@ int makesub(char* arg, int from, character delim, char* sub){
}
-/*@ 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){
+char getsub(char* arg, char* sub){
int makeres;
- makeres = makesub(arg, 0, ENDSTR, sub);
+ makeres = makesub(arg, 0, '\0', sub);
+ //@ ghost char* tmp_arg = arg;
+ //@ ghost char* tmp_sub = sub;
+ //@ ghost int verdict = 1;
+ /*@ ghost while (*tmp_arg != 0) {
+ if(*tmp_arg == '&') {
+ if(*tmp_sub != -1){verdict=0;break;}
+ tmp_arg++; tmp_sub++;
+ }
+ else if(*tmp_arg == '@' && *(tmp_arg+1) == '\0') {
+ if(*tmp_sub != '@') {verdict=0;break;}
+ tmp_arg++; tmp_sub++;
+ }
+ else if(*tmp_arg == '@' && *(tmp_arg+1) == 'n') {
+ if(*tmp_sub != 10) {verdict=0;break;}
+ tmp_arg += 2; tmp_sub++;
+ }
+ else if(*tmp_arg == '@' && *(tmp_arg+1) == 't') {
+ if(*tmp_sub != 9) {verdict=0;break;}
+ tmp_arg += 2; tmp_sub++;
+ }
+ else if(*tmp_arg == '@') {
+ if(*tmp_sub != *(tmp_arg+1)) {verdict=0;break;}
+ tmp_arg += 2; tmp_sub++;
+ }
+ else {
+ if(*tmp_sub != *tmp_arg) {verdict=0;break;}
+ tmp_arg++; tmp_sub++;
+ }
+ } */
+
+ //@ assert verdict == 1;
if(makeres > 0){
+ //@ assert makeres > 0;
return(1);
}
else{
+ //@ assert makeres <= 0;
return(0);
}
}
-
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/oracle_getsub.c b/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/oracle_getsub.c
new file mode 100644
index 0000000000000000000000000000000000000000..5874b006dad5c90fb1f4b03269df2687d4357694
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/oracle_getsub.c
@@ -0,0 +1,36 @@
+
+#include "string.h"
+
+void oracle_getsub(char* Pre_arg, char* arg, char* Pre_sub, char* sub, int r) {
+ char* tmp_arg = Pre_arg;
+ char* tmp_sub = sub;
+ while(*tmp_arg != 0) {
+ if(*tmp_arg == '&') {
+ if(*tmp_sub != -1) {pathcrawler_verdict_failure();return;}
+ tmp_arg++; tmp_sub++;
+ }
+ else if(*tmp_arg == '@' && *(tmp_arg+1) == '\0') {
+ if(*tmp_sub != '@') {pathcrawler_verdict_failure();return;}
+ tmp_arg++; tmp_sub++;
+ }
+ else if(*tmp_arg == '@' && *(tmp_arg+1) == 'n') {
+ if(*tmp_sub != 10) {pathcrawler_verdict_failure();return;}
+ tmp_arg += 2; tmp_sub++;
+ }
+ else if(*tmp_arg == '@' && *(tmp_arg+1) == 't') {
+ if(*tmp_sub != 9) {pathcrawler_verdict_failure();return;}
+ tmp_arg += 2; tmp_sub++;
+ }
+ else if(*tmp_arg == '@') {
+ if(*tmp_sub != *(tmp_arg+1)) {pathcrawler_verdict_failure();return;}
+ tmp_arg += 2; tmp_sub++;
+ }
+ else {
+ if(*tmp_sub != *tmp_arg) {pathcrawler_verdict_failure();return;}
+ tmp_arg++; tmp_sub++;
+ }
+ }
+
+ pathcrawler_verdict_success();
+ return;
+}
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
index 52766e82aebdab9eb080059f9e659bd2f46bb59c..a1e94895895e5a07994e9f7754d47b71482aaa01 100644
--- 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
@@ -17,15 +17,15 @@ dom('getsub',cont('sub__getsub',_),[],int([-128..127])).
% 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),
+ create_input_val(dim('sub__getsub'),int([6..6]),Ins),
+ create_input_val(dim('arg__getsub'),int([6..6]),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)]).
+unquantif_preconds('getsub',[cond(egal,cont('sub__getsub',5),0,pre),
+ cond(egal,cont('arg__getsub',5),0,pre)]).
quantif_preconds('getsub',[]).