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

[Frama-c-discuss] assigns \from supported in WP?



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>