Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] assigns \from supported in WP?
  • From: loic.correnson at cea.fr (Loïc Correnson)
  • Date: Fri, 31 Jan 2014 15:15:16 +0100
  • In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C76682E471@Mail1.FCMD.local>
  • References: <B517F47C2F6D914AA8121201F9EBEE6701C76682E471@Mail1.FCMD.local>
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>