--- layout: fc_discuss_archives title: Message 61 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



On Fri, 2011-02-18 at 13:23 +0100, Virgile Prevosto wrote:
> context. That said, the error should be logic label P not found. Could
> you give a complete example that reproduce your issue?
>

Sorry, yes, my original example doesn't makes much sense.

The following code verifies, but the specification
unchanged{P,H}(\at(&this->a, P)); is quite clumsy.


typedef int bool;

/*@ predicate unchanged{P,H}(bool* p) =
		\at(*p, P) <==> \at(*p, H);
*/

typedef struct {
	bool a;
} S_t;


/*@ predicate foo_spec{P,H}(S_t* this) =
		unchanged{P,H}(\at(&this->a, H));
*/
/*@	ensures foo_spec{Pre,Here}(this);
*/
void foo(S_t* this)
{
	;
}


If write &this->a instead of \at(&this->a, H), frama-c complains "no label
in the context". In Patrick's example, the pointer is given with an \at:

//@ensures bar_spec{Here,Old}(&x) ;

Is &x automatically interpreted as \at(&x, Here) in this context?

Regards,
Boris