--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on February 2011 ---
[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