--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on January 2010 ---
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