Newer
Older
/* run.config*
OPT: -aorai-buchi @PTEST_DIR@/@PTEST_NAME@.promela -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-buchi %{dep:@PTEST_DIR@/test_recursion3.promela} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
//========================
// Strings
//--------
//
/*@ axiomatic string_len {
logic integer string_len{L}(char *s);
axiom strlen0{L}: \forall char *s ; \valid(s) ==> string_len(s)>=0;
axiom strlen1{L}: \forall char *s ; \valid(s) && s[0]=='\0' ==> string_len(s)==0 ;
axiom strlen2{L}: \forall char *s ; \valid(s) ==> s[string_len(s)]=='\0' ;
axiom strlen3{L}: \forall char *s ; \valid(s) && s[0]!='\0' ==> string_len(s)==1+string_len(s+1) && \valid(s+1) ;
axiom strlen4{L}: \forall char *s ; \valid(s) ==>
\forall integer i ; 0<=i<string_len(s) ==> s[i]!='\0' ;
}
*/
/*@ predicate valid_string{L}(char *s) =
\valid(s) && \valid(s+(0 .. string_len(s))) ;
*/
//
//
//========================
// Sum of a tab
//-------------
//
/*@ axiomatic sum_tab {
logic integer sum_tab{L}(char *t,integer l,integer i);
axiom sum_tab0{L}:
\forall char *t, integer l ;
\valid(t + (0 .. l)) ==> sum_tab(t,l,0)==t[0];
axiom sum_tabi{L}:
\forall char *t, integer l, integer i ;
\valid(t + (0 .. l)) && 0<i<=l ==>
sum_tab(t,l,i)==sum_tab(t,l,i-1)+t[i];
axiom sum_tabn{L}:
\forall char *t, integer l ;
\valid(t + (0 .. l)) && l>0 && l==string_len(t) ==>
sum_tab(t,l,l)==sum_tab(t,l,l-1);
}
*/
//
//========================
int global_argc=0;
/* Calcul de la longueur d'une chaine */
/*@ requires valid_string(argv);
@ ensures \result==string_len(argv);
*/
int count(char* argv) {
if(argv[0]==0) return 0;
return 1+count(argv+1);
}
/*@ requires valid_string(t) && length>=0 && length==string_len(t);
@ ensures \result==sum_tab(t,length,length);
*/
int sumOne(char* t, int length) {
// printf(" --> t : '%s' / length : %d\n",t,length);
int sum=0;
int i=0;
//printf(" ----> c = '%d'\n",t[i]);
/*@ loop invariant ranges: 0<=i<=length;
@ loop invariant sumValue0: i==0 ==> sum==0;
@ loop invariant sumValuei: i>0 ==> sum==sum_tab(t,length,i-1);
*/
for(i=0;i<length;i++){
//printf(" ----> c = '%d'\n",t[i]);
sum+=t[i];
}
return sum;
}
/*@ requires argc>=0 && (argc>0 ==> \valid(argv) && valid_string(argv[0]));
@ ensures \result==1;
*/
int main(int argc, char** argv) {
int sum=0;
int length;
global_argc=argc;
if (argc>0) {
length=count(argv[0]);
sum=sumOne(argv[0],length);
}
//printf("Somme cumulee du premier param = %d\n",sum);
return 1;
}