update wrt AST change (new constructor GFunDecl)

src/plugins/e-acsl/dup_functions.ml

@@ -281,7 +281,7 @@ class dup_functions_visitor prj = object (self)
     | _ -> false
 
   method !vglob_aux = function
-  | GVarDecl(_, vi, loc) | GFun({ svar = vi }, loc)
+  | GVarDecl(vi, loc) | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
       when self#is_unvariadic_function vi
 	&& not (Misc.is_library_loc loc) 
 	&& not (Cil.is_builtin vi)
@@ -298,9 +298,10 @@ class dup_functions_visitor prj = object (self)
     Cil_datatype.Varinfo.Hashtbl.add fct_tbl vi new_vi;
     Cil.DoChildrenPost
       (fun l -> match l with
-      | [ GVarDecl(_, vi, _) | GFun({ svar = vi }, _) as g ] -> 
+      | [ GVarDecl(vi, _) | GFunDecl(_, vi, _) | GFun({ svar = vi }, _) as g ]
+        ->
 	(match g with
-	| GVarDecl _ ->
+        | GFunDecl _ ->
 	  if not (Kernel_function.is_definition (Extlib.the self#current_kf))
             && vi.vname <> "malloc" && vi.vname <> "free" 
           then
@@ -334,14 +335,16 @@ if there are memory-related annotations.@]"
 	in
 	self#dup_libc g new_g
       | _ -> assert false)
-  | GVarDecl(_, _, loc) | GFun(_, loc) when Misc.is_library_loc loc ->
+  | GVarDecl(_, loc) | GFunDecl(_, _, loc) | GFun(_, loc)
+      when Misc.is_library_loc loc ->
     (match before_memory_model with
     | Before_gmp -> before_memory_model <- Gmp
     | Gmp | Memory_model -> ()
     | After_gmp -> before_memory_model <- Memory_model
     | Code -> assert false);
     Cil.JustCopy
-  | GVarDecl(_, vi, _) | GFun({ svar = vi }, _) when Cil.is_builtin vi ->
+  | GVarDecl(vi, _) | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
+      when Cil.is_builtin vi ->
     self#next ();
     Cil.JustCopy
   | _ -> 

src/plugins/e-acsl/visit.ml

@@ -253,7 +253,8 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
 	 f)
 
   method !vglob_aux = function
-  | GVarDecl(_, vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _) 
+  | GVarDecl(vi, _) | GVar(vi, _, _)
+  | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
       when Misc.is_library_loc vi.vdecl ->
     if generate then
       Cil.JustCopyPost
@@ -264,7 +265,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
       Misc.register_library_function vi; 
       Cil.SkipChildren
     end
-  | GVarDecl(_, vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _) 
+  | GVarDecl(vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
       when Cil.is_builtin vi ->
     if generate then Cil.JustCopy else Cil.SkipChildren
   | g when Misc.is_library_loc (Global.loc g) ->
@@ -289,7 +290,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
            [vfile]) *)
         if vi.vorig_name = Kernel.MainFunction.get () then
           main_fct <- Some fundec
-      | GVarDecl(_, vi, _) -> 
+      | GVarDecl(vi, _) | GFunDecl(_, vi, _) ->
         (* do not convert extern ghost variables, because they can't be linked,
            see bts #1392 *)
         if vi.vstorage <> Extern then
@@ -298,7 +299,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
         ()
     in
     (match g with
-    | GVar(vi, _, _) | GVarDecl(_, vi, _) -> 
+    | GVar(vi, _, _) | GVarDecl(vi, _) ->
       Varinfo.Hashtbl.replace global_vars vi None
     | _ -> ());
     if generate then Cil.DoChildrenPost(fun g -> List.iter do_it g; g)