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] 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