Extract Cilfacade.sync_formals

Author: sim642

src/autoTune.ml

@@ -321,10 +321,7 @@ let selectArrayDomains file =
   set_bool "annotation.goblint_array_domain" true;
   let thisVisitor = new addTypeAttributeVisitor in
   ignore (visitCilFileSameGlobals thisVisitor file);
-  (* Sync formal parameter attributes back to function types for correct CIL printing *)
-  iterGlobals file (function
-      | GFun (fd, _) -> setFormals fd fd.sformals
-      | _ -> ())
+  Cilfacade.sync_formals file
 (*small unrolled loops also set domain of accessed arrays to unroll, at the point where loops are unrolled*)
 
 
@@ -460,10 +457,7 @@ let apronOctagonOption factors file =
     Logs.info "Enabled octagon domain ONLY for:";
     Logs.info "%s" @@ String.concat ", " @@ List.map (fun info -> info.vname) allVars;
     List.iter (fun info -> info.vattr <- addAttribute (Attr("goblint_relation_track",[])) info.vattr) allVars;
-    (* Sync formal parameter attributes back to function types for correct CIL printing *)
-    iterGlobals file (function
-        | GFun (fd, _) -> setFormals fd fd.sformals
-        | _ -> ())
+    Cilfacade.sync_formals file
   in
   {
     value = 50 * (List.length allVars) ;

src/common/util/cilfacade.ml

@@ -827,6 +827,13 @@ let add_function_declarations (file: Cil.file): unit =
   let globals = upto_last_type @ fun_decls @ non_types @ functions in
   file.globals <- globals
 
+(** Sync formal parameter attributes back to function types for correct CIL printing *)
+let sync_formals file =
+  iterGlobals file (function
+      | GFun (fd, _) -> setFormals fd fd.sformals
+      | _ -> ()
+    )
+
 
 (** Special index expression for some unknown index.
     Weakly updates array in assignment.