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