--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on April 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about treatment of assigns clauses in WP (Neon)



Hello Virgile, Pascal, and  Patrick,

thanks for your replies!

> the point is
> just to check that all occurrences of *p in assigns are guarded by a
> \valid(p) in requires.

That?s exactly what I mean!

> It'd just act as a consistency check for the
> specification itself, without any reference to an implementation which
> might not even exist in the first place.
> 

Jens