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

[Frama-c-discuss] annotations and value analysis



Hello again,

> The assigns clause with dependencies is interpreted
> by the value analysis, but at this time, the pre- and
> post-conditions are not.

It turned out that preconditions had been supported in
the value analysis for library function contracts for
a long time, probably already in 20090902.

The development version now has preliminary,
little-tested support for post-conditions, too.
St?phane, if you play with this, keep an eye open
for strange behaviors and keep us informed.

Don't start holding your breath for \result jus yet, though.

Best regards,

Pascal