Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with predicate and location labels

Hello Boris,

Le jeu. 17 f?vr. 2011 10:03:40 CET,
Boris Hollas <hollas at informatik.htw-dresden.de> a ?crit :

> Assume I have a function foo that calls another function bar. I want to
> write a contract for foo such as
> 
> ensures bar_spec(this->a);
> 
> where bar_spec also specifies variables that remain unchanged and
> bar_spec may contain specifications of functions called by bar. Thus,
> the specification of function foo contains the union of all functions
> transitively called by foo. 
> So far, I use the preprocessor to accomplish this. Is there a more
> elegant way to do this?

I'm not completely sure that this can be done safely in a fully general
setting. In the general case, you have to do some weakest-precondition
computation to lift the specification of bar from the call point up to
the starting point of foo. e.g. with

void foo(struct S* arr, int length) {
struct S* this;
for (int i = 0; i<length; i++) {
 this = arr+i;
 foo(this->a);
}
}

even assuming that we have a way to express bar_spec, your spec of foo
is not ensures bar_spec(this->a) but rather 
ensures \forall integer i; 0<=i<length ==> bar_spec((arr+i)->a);

which is not something that a pre-processor is likely to produce.

An easier thing to do is to transform the spec of foo into a statement
contract at the call point. This is -among other things- what the RTE
plugin (in Carbon beta and beyond) is doing when the -rte-precond
option is on. As I said, going further would pretty much require
writing a weakest-precondition computation plugin operating at C/ACSL
level

-- 
E tutto per oggi, a la prossima volta.
Virgile