I am trying to generate contracts in C with E-ACSL plugin from FRAMA-C for the following program:
struct lnode {
int value;
struct lnode *next;
};
struct set {
int capacity;
int size;
struct lnode *elems;
};
struct set* new(int capacity) {
struct set *new_set;
new_set = (struct set*) malloc(sizeof(struct set));
if(new_set == NULL)
return NULL; /* no memory left */
new_set->capacity = capacity;
new_set->size = 0;
new_set->elems = NULL;
return new_set;
}
int insert(struct set *s, int x) {
struct lnode *new_node;
struct lnode *end_node;
struct lnode *n;
if(s==NULL)
return 0; /* NULL set */
if(s->size >= s->capacity)
return 0; /* no space left */
end_node = s->elems;
n = end_node;
while(n != NULL) {
if(n->value == x)
return 0; /* element already in the set */
end_node = n;
n = n->next;
}
/* Creation of new node */
new_node = (struct lnode*) malloc(sizeof(struct lnode));
if(new_node == NULL)
return 0; /* no memory left */
new_node->value = x;
new_node->next = s->elems;
s->elems = new_node;
s->size += 1;
return 1; /* element added */
}
int isnull(struct set *s) {
if(s==NULL)
return 1;
return 0;
}
int isempty(struct set *s) {
if(s==NULL)
return 0;
if(s->elems==NULL)
return 1; /* s is empty */
return 0;
}
int isfull(struct set *s) {
if(s==NULL)
return 0;
if(s->size >= s->capacity)
return 1; /* s is full */
return 0;
}
int contains(struct set *s, int x) {
struct lnode *n;
if(s==NULL)
return 0; /* s is NULL */
n = s->elems;
while(n != NULL){
if(n->value == x)
return 1; /* element found */
n = n->next;
}
return 0; /* element NOT found */
}
int length(struct set *s) {
struct lnode *n;
int count;
if(s==NULL)
return 0; /* s is NULL */
count = 0;
n = s->elems;
while(n != NULL){
count = count + 1;
n = n->next;
}
return count;
}
The ACSL manual (Section 2.3.2) says the correct way to do it is by adding an annotation before the function. However, in my specification I intend to include predicates that use program's functions to define a final axiom for the insert function. For example:
@ requires \valid(s);
@ behavior A:
@ ensures (isfull(s)=0 && length(s)=0 && contains(s,x)=0 && isnull(s)=0 && isempty(s)=1) ==>
(length(s)=1 && contains(s,x)=1 && isnull(s)=0 && isempty(s)=0 && \result==1);
When I try to compile using e-acsl-gcc.sh I get this error:
user@ubuntu-tmpl:~/Documents/Code$ e-acsl-gcc.sh -c insert.c -O exec
++ frama-c -variadic-no-translation -machdep gcc_x86_64 '-cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 ' -no-frama-c-stdlib insert.c axiomTes.c -e-acsl -e-acsl-share=/home/user/.opam/system/bin/../share/frama-c/e-acsl/ -then-last -print -ocode a.out.frama.c
[kernel] Parsing FRAMAC_SHARE/e-acsl//e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl//e_acsl.h (with preprocessing)
[kernel] Parsing insert.c (with preprocessing)
insert.c:31:[kernel] user error: unbound function isempty
[kernel] user error: stopping on file "insert.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
e-acsl-gcc: fatal error: aborted by Frama-C
This leads me to think function call either is not allowed inside the annotation or has another syntax spec. Is it any way to use the program's defined functions to form the predicates? Another possibility which is still suitable for me is to get the result of the function call somewhere else and use it inside the annotation.
Thanks!
First of all, it would be much easier for us to answer if you give the exact code on which you've tried to launch e-acsl, including its annotations. Putting these apart, without enclosing them properly in comments only means that it's more complicated to reproduce the issue, and that we can't be sure that we are reproducing exactly your setup.
That said, here are the issues that I've spotted by looking at the annotation above (without launching frama-c on it for the reasons previously stated).
Indeed, you cannot call a C function into an ACSL annotation. It is possible to define logic functions and predicates in ACSL, though, that you can then use in annotations (after having defined them of course). This is described in the ACSL manual, section 2.6, and ACSL by Example contains many examples of them.
In ACSL, as in C, equality is denoted by ==, not =.
It might be a good idea to split your ensures into many clauses instead
of having a single clause which is a conjunction: it would make it easier to find which part of the post-condition is not validated.
Similarly, unless you want to complete the contract, the behavior A: does not serve any real purpose.
On a stylistic side, @ is only mandatory to introduce an annotation (with /*@ ... */). You do not need to put one on each line.