--- layout: fc_discuss_archives title: Message 72 from Frama-C-discuss on September 2009 ---
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