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] ACSL contracts lost during GFun modification in Ast Copy

  • Subject: [Frama-c-discuss] ACSL contracts lost during GFun modification in Ast Copy
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
  • Date: Fri, 28 Oct 2011 17:37:34 +0200
  • In-reply-to: <569C6D7D26484241A530B87F45ADE1F87E5E5B@AOFRWMBXRSC004.resources.atosorigin.local>
  • References: <569C6D7D26484241A530B87F45ADE1F87E5E5B@AOFRWMBXRSC004.resources.atosorigin.local>
Hello St?phane,

On 28/10/2011 17:04, DUPRAT Stephane wrote:
> Hello,
>
> I'm working on a new Frama-C project built by the cmd
> "File.create_project_from_visitor" and I lose the ACSL contract if a
> make a change to a global function.
>
> For example, if have a copy visitor like this:
>
> inherit Visitor.frama_c_copy prj method vglob_aux g = match g with |
> GFun (_)  -> Cil.ChangeTo [g]
>
> All functions have lost their contract in the copy project. Is there
> a way to keep contracts of the original function ? Perhaps throw the
> kernel_functions, but they are not handle by the visitor.
>

As a rule of thumb, whenever you use SkipChildren or ChangeTo in a 
visitor, the visit stop there. In particular, since a function contract 
is considered somehow as a child of the global it belongs to, the 
contract will not be visited, (and not copied in the new project when 
you have a copy visitor).

By the way, the use of ChangeTo in your code snippet is incorrect: the 
function (and in particular its statements, the varinfos of formals and 
globals, etc.) are shared between original and new projects. In fact, 
ChangeTo g should only be used in a copy visitor if g has been built 
from scratch by the visitor (that must also add to the action queue the 
registration of the new contract if needed). Developer's manual suggests 
to use ChangeDoChildrenPost(g,fun x -> x) instead, to ensure that all 
the nodes will be visited and copied.

Best regards,
--
E tutto per oggi, a la prossima volta
Virgile