--- layout: fc_discuss_archives title: Message 72 from Frama-C-discuss on September 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem between Project change and modifying Ast information through visitors



Hello Pierre-Lo?c,

Pierre-Lo?c Garoche a ?crit :
> I'm trying to update some information of the ast using the visitors provided in the Frama-C API.
> I followed the exemple of the plugin dev manual without success.
> 
> My goal is just to update the value of the mutable annotation status.

As Anne suggests, you should simply use the function 
Db.Properties.Status.CodeAnnotation.update introduced in the new 
Beryllium 2.

There is no need of a visitor here.

> class status_update_visitor = object ( self )
>   inherit Visitor.frama_c_inplace
> 
>   method vcode_annot annot =
> 	match annot.annot_content with
> 	    | AAssert (_,_,annot_status) -> annot_status.status <- a_new_value_for_this_status
> 	    | _ -> Self.fatal "Found a code annotation that is not an assert"
> 	Cil.DoChildren
> end
> 
> I use two different projects. The call of this visitor works and modify the Ast. However if I change to the second project
> 	Project.set_current prj2
> the modification disappear. The problem is that going back to the first project doesn't solve the problem.

An AST must never be modified inside a project (see plug-in development 
guide, p. 50).

Another key point is that you must never use annotations contained in 
the AST. You must use the ones that are stored in Frama-C tables (module 
Annotations or Globals.Annotations or Db.Properties.Status.* depending 
on what you need). Maybe it should be better documented.

Consequently you are outside the Frama-C specifications, so you get 
strange results ;).

Hope this helps,
Julien