Deduplicate preprocessing

src/analyses/loopTermination.ml

@@ -99,5 +99,5 @@ struct
 end
 
 let () =
-  Cilfacade.register_preprocess_cil (Spec.name ()) (new loopCounterVisitor loop_counters);
+  Cilfacade.register_preprocess (Spec.name ()) (new loopCounterVisitor loop_counters);
   MCP.register_analysis (module Spec : MCPSpec)

src/common/util/cilfacade.ml

@@ -74,27 +74,13 @@ let print (fileAST: file) =
 let rmTemps fileAST =
   RmUnused.removeUnused fileAST
 
-
 let visitors = ref []
 let register_preprocess name visitor_fun =
   visitors := !visitors @ [name, visitor_fun]
 
 let do_preprocess ast =
-  let f fd (name, visitor_fun) =
-    (* this has to be done here, since the settings aren't available when register_preprocess is called *)
-    if List.mem name (get_string_list "ana.activated") then
-      ignore @@ visitCilFunction (visitor_fun fd) fd
-  in
-  iterGlobals ast (function GFun (fd,_) -> List.iter (f fd) !visitors | _ -> ())
-
-let visitors_cil = ref []
-(* does exactly the same as register_preprocess but it is executed earlier, before the CFG is created*)
-let register_preprocess_cil name visitor_fun =
-  visitors_cil := !visitors_cil @ [name, visitor_fun]
-
-let do_preprocess_cil ast =
   (* this has to be done here, since the settings aren't available when register_preprocess is called *)
-  let active_visitors = List.filter_map (fun (name, visitor_fun) -> if List.mem name (get_string_list "ana.activated") then Some visitor_fun else None) !visitors_cil in
+  let active_visitors = List.filter_map (fun (name, visitor_fun) -> if List.mem name (get_string_list "ana.activated") then Some visitor_fun else None) !visitors in
   let f fd visitor_fun = ignore @@ visitCilFunction (visitor_fun fd) fd in
   if active_visitors <> [] then
     iterGlobals ast (function GFun (fd,_) -> List.iter (f fd) active_visitors | _ -> ())

src/util/cilCfg.ml

@@ -42,6 +42,7 @@ let loopCount file =
 
 
 let createCFG (fileAST: file) =
+  Cilfacade.do_preprocess fileAST;
   (* The analyzer keeps values only for blocks. So if you want a value for every program point, each instruction      *)
   (* needs to be in its own block. end_basic_blocks does that.                                                        *)
   (* After adding support for VLAs, there are new VarDecl instructions at the point where a variable was declared and *)
@@ -50,7 +51,6 @@ let createCFG (fileAST: file) =
   (* Since we want the output of justcil to compile, we do not run allBB visitor if justcil is enable, regardless of  *)
   (* exp.basic-blocks. This does not matter, as we will not run any analysis anyway, when justcil is enabled.         *)
   (* the preprocessing must be done here, to add the changes of CIL to the CFG*)
-  Cilfacade.do_preprocess_cil fileAST;
   if not (get_bool "exp.basic-blocks") && not (get_bool "justcil") then end_basic_blocks fileAST;
 
   (* We used to renumber vids but CIL already generates them fresh, so no need.
@@ -68,6 +68,4 @@ let createCFG (fileAST: file) =
         computeCFGInfo fd true
       | _ -> ()
     );
-  if get_bool "dbg.run_cil_check" then assert (Check.checkFile [] fileAST);
-
-  Cilfacade.do_preprocess fileAST
+  if get_bool "dbg.run_cil_check" then assert (Check.checkFile [] fileAST);