diff --git a/src/analyses/loopTermination.ml b/src/analyses/loopTermination.ml index f4db165795..312bcfd9b9 100644 --- a/src/analyses/loopTermination.ml +++ b/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) diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 47cf6d6210..d645fd949d 100644 --- a/src/common/util/cilfacade.ml +++ b/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 | _ -> ()) diff --git a/src/util/cilCfg.ml b/src/util/cilCfg.ml index 72143e97d7..923cf7600b 100644 --- a/src/util/cilCfg.ml +++ b/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); \ No newline at end of file