Merge branch 'fix/kernel/code-transformation' into 'master'

[kernel] Always recompute the CFG after applying a code transformation.

See merge request frama-c/frama-c!3214

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

tests/misc/oracle/ulevel.res.oracle

+[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.
+  ----------------------------------------------------------------------------

tests/misc/ulevel.i

+/* 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++)
+      ;
+}