[e-acsl:archi] fix bug with global compound initializers

src/plugins/e-acsl/src/code_generator/global_observer.ml

@@ -178,6 +178,6 @@ let mk_delete_stmts stmts =
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)

src/plugins/e-acsl/src/code_generator/injector.ml

@@ -60,11 +60,14 @@ let rec inject_in_init env kf_opt vi off = function
     let e, env = replace_literal_string_in_exp env kf_opt e in
     SingleInit e, env
   | CompoundInit(typ, l) ->
+    (* inject in all single initializers that can be built from the compound
+       version *)
     let l, env =
       List.fold_left
-        (fun (l, env) (off, i) ->
-           let i, env = inject_in_init env kf_opt vi off i in
-           (off, i) :: l, env)
+        (fun (l, env) (off', i) ->
+           let new_off = Cil.addOffset off' off in
+           let i, env = inject_in_init env kf_opt vi new_off i in
+           (off', i) :: l, env)
         ([], env)
         l
     in
@@ -588,7 +591,9 @@ let inject_in_fundec main fundec =
   List.iter (fun vi -> vi.vghost <- false) fundec.slocals;
   (* update environments *)
   Builtins.update vi.vname vi;
-  if is_main kf then Global_observer.add vi;
+  (* track function addresses but the main function that is tracked internally
+     via RTL *)
+  if not (is_main kf) then Global_observer.add vi;
   (* exit point computations *)
   if Functions.instrument kf then Exit_points.generate fundec;
   Options.feedback ~dkey ~level:2 "entering in function %a."
@@ -629,6 +634,7 @@ let inject_in_global (env, main) = function
     (* do not convert extern ghost variables, because they can't be linked,
        see bts #1392 *)
     if vi.vstorage <> Extern then vi.vghost <- false;
+    Global_observer.add vi;
     env, main
 
   (* variable definition *)

src/plugins/e-acsl/src/code_generator/temporal.ml

@@ -138,7 +138,7 @@ let assign ?(ltype) lhs rhs loc =
      via [Cil.typeOfLval] later *)
   let ltype = match ltype with
     | Some l -> l
-    | None -> (Cil.typeOfLval lhs)
+    | None -> Cil.typeOfLval lhs
   in
   match Cil.unrollType ltype with
   | TPtr _ ->
@@ -514,14 +514,12 @@ let handle_stmt stmt env kf =
     env
 
 let generate_global_init vi off init =
-  if is_enabled () then
-    mk_global_init ~loc:vi.vdecl vi off init
-  else
-    None
+  if is_enabled () then mk_global_init ~loc:vi.vdecl vi off init
+  else None
 (* }}} *)
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)

src/plugins/e-acsl/tests/temporal/t_global_init.c

@@ -14,7 +14,7 @@ struct tree_desc2 {
 
 typedef struct tree_desc2 tree_desc2;
 
-static int extra_lbits[] = {0};
+static int extra_lbits[] = { 0 };
 
 static tree_desc l_desc =
   /* This bit should be tracked via globals_init function */
@@ -59,6 +59,3 @@ int main(int argc, const char **argv) {
 
     return 0;
 }
-
-
-