diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml index 8d5ce416adc74c1837981b6b097af5aed429dc8f..c71b094486f17fc7bbd2bb146716097f51c9583e 100644 --- a/src/kernel_services/ast_queries/file.ml +++ b/src/kernel_services/ast_queries/file.ml @@ -1026,6 +1026,23 @@ let register_code_transformation_category s = after_id = Transform_after_cleanup.register_key s; prm_id = Transform_after_parameter_change.register_key s } +module Cfg_recomputation_queue = + State_builder.Set_ref(Cil_datatype.Fundec.Set) + (struct + let name = "File.Cfg_recomputation_queue" + let dependencies = [Ast.self] + end) + +let () = Ast.add_linked_state Cfg_recomputation_queue.self + +let must_recompute_cfg f = Cfg_recomputation_queue.add f + +let recompute_cfg _ = + (* just in case f happens to modify the CFG *) + Cfg_recomputation_queue.iter + (fun f -> Cfg.clearCFGinfo ~clear_id:false f; Cfg.cfgFun f); + Cfg_recomputation_queue.clear () + let add_transform_parameter ~before ~after name f (p:(module Parameter_sig.S)) = let module P = (val p: Parameter_sig.S) in @@ -1037,6 +1054,7 @@ let add_transform_parameter "applying %s to current AST, after option %s changed" name.name P.option_name; f (Ast.get()); + recompute_cfg (); if Kernel.Check.get () then Filecheck.check_ast ("after code transformation: " ^ name.name ^ @@ -1058,23 +1076,6 @@ let add_transform_parameter Transform_after_parameter_change.add_dependency a.prm_id name.prm_id) after -module Cfg_recomputation_queue = - State_builder.Set_ref(Cil_datatype.Fundec.Set) - (struct - let name = "File.Cfg_recomputation_queue" - let dependencies = [Ast.self] - end) - -let () = Ast.add_linked_state Cfg_recomputation_queue.self - -let must_recompute_cfg f = Cfg_recomputation_queue.add f - -let recompute_cfg _ = - (* just in case f happens to modify the CFG *) - Cfg_recomputation_queue.iter - (fun f -> Cfg.clearCFGinfo ~clear_id:false f; Cfg.cfgFun f); - Cfg_recomputation_queue.clear () - let transform_and_check name is_normalized f ast = let printer = if is_normalized then Printer.pp_file else Cil_printer.pp_file diff --git a/tests/misc/oracle/ulevel.res.oracle b/tests/misc/oracle/ulevel.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..8c985ade07737ebb5447af9211ea40365e3309cb --- /dev/null +++ b/tests/misc/oracle/ulevel.res.oracle @@ -0,0 +1,24 @@ +[kernel] Parsing tests/misc/ulevel.i (no preprocessing) +[eva] Analyzing a complete application starting at main +[eva] Computing initial state +[eva] Initial state computed +[eva:initial-state] Values of globals at initialization + +[eva] tests/misc/ulevel.i:12: starting to merge loop iterations +[eva] tests/misc/ulevel.i:11: starting to merge loop iterations +[eva] done for function main +[eva] ====== VALUES COMPUTED ====== +[eva:final-states] Values at end of function main: + i ∈ {4} + j ∈ {3} +[eva:summary] ====== ANALYSIS SUMMARY ====== + ---------------------------------------------------------------------------- + 1 function analyzed (out of 1): 100% coverage. + In this function, 31 statements reached (out of 33): 93% coverage. + ---------------------------------------------------------------------------- + No errors or warnings raised during the analysis. + ---------------------------------------------------------------------------- + 0 alarms generated by the analysis. + ---------------------------------------------------------------------------- + No logical properties have been reached by the analysis. + ---------------------------------------------------------------------------- diff --git a/tests/misc/ulevel.i b/tests/misc/ulevel.i new file mode 100644 index 0000000000000000000000000000000000000000..1f6833afd71361621b270143335b2c90fea0fec9 --- /dev/null +++ b/tests/misc/ulevel.i @@ -0,0 +1,14 @@ +/* run.config + OPT: -then -ulevel-force -eva + */ + +/* Tests the syntaxic loop unrolling when triggered by an option change + (here -ulevel-force) and not at the first parsing. */ + +void main(void) { + int i, j; + /*@ loop pragma UNROLL 1; */ + for(i = 0; i < 4; i++) + for(j = 0; j < 3; j++) + ; +}