--- layout: fc_discuss_archives title: Message 103 from Frama-C-discuss on January 2014 ---
Well, There is an article from our lab?[1] describing (and proving the soundness of) a method for verifying ?\from` specifications with WP. A prototype of the solution was implemented in the past. However, with the recent refactoring of WP internals, we were obliged to temporary disconnect it from the maintained code. In the meanwhile, other solutions have been envisioned to address this issue. Today, we technically have no ready-to-implement solution for proving \from using WP. However, it seems to be possible, although with heavy developments. Regards, L. Correnson [1] Pascal Cuoq, Benjamin Monate, Anne Pacalet and Virgile Prevosto Functional Dependencies of C Functions via Weakest Pre-Conditions Software Tools for Technology Transfer, 13:5, October 2011 https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:functional_dependencies Le 30 janv. 2014 ? 18:49, Dharmalingam Ganesan <dganesan at fc-md.umd.edu> a ?crit : > Hi, > > I'm reading Section 7.2 (http://frama-c.com/download/frama-c-value-analysis.pdf) > > I'm curious whether WP can verify whether assigns \from... > > I got a warning that it ignores \from part of the specification? > > Is it possible at all to verify whether the assigns rule with \from is actually followed in the implementation? > > Thanks, > Dharma > > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140131/d4d969c4/attachment.html>