--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on October 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL contracts lost during GFun modification in Ast Copy



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