[eacsl] Add helper functions to initialize structures

- `Smart_stmt.struct_local_init` creates a `Local_init` statement to
  initialize a structure
- `Smart_stmt.assigns_field` creates a statement to assigns a value to a
  field of a structure.

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

@@ -34,11 +34,61 @@ let call_instr ~loc ?result e args = instr (Call(result, e, args, loc))
 
 let assigns ~loc ~result e = instr (Set(result, e, loc))
 
+let assigns_field ~loc vi name value =
+  let ty = vi.vtype in
+  let compinfo =
+    match Cil.unrollType ty with
+    | TComp (compinfo, _, _) -> compinfo
+    | _ ->
+      Options.fatal
+        "type of %a (%a) is not a structure"
+        Printer.pp_varinfo vi
+        Printer.pp_typ ty
+  in
+  let field =
+    try
+      Cil.getCompField compinfo name
+    with Not_found ->
+      Options.fatal
+        "Unable to find field '%s' in structure '%a'"
+        name
+        Printer.pp_typ ty
+  in
+  let result = Var vi, (Field (field, NoOffset)) in
+  assigns ~loc ~result value
+
 let if_stmt ~loc ~cond ?(else_blk=Cil.mkBlock []) then_blk =
   stmt (If (cond, then_blk, else_blk, loc))
 
 let break ~loc = stmt (Break loc)
 
+let struct_local_init ~loc vi fields =
+  vi.vdefined <- true;
+  let ty = vi.vtype in
+  let compinfo =
+    match Cil.unrollType ty with
+    | TComp (compinfo, _, _) -> compinfo
+    | _ ->
+      Options.fatal
+        "type of %a (%a) is not a structure"
+        Printer.pp_varinfo vi
+        Printer.pp_typ ty
+  in
+  let fields =
+    List.map
+      (fun (name, e) ->
+         try
+           let field = Cil.getCompField compinfo name in
+           Field (field, NoOffset), SingleInit e
+         with Not_found ->
+           Options.fatal
+             "Unable to find field '%s' in structure '%a'"
+             name
+             Printer.pp_typ ty)
+      fields
+  in
+  instr (Local_init (vi, AssignInit (CompoundInit (ty, fields)), loc))
+
 let block stmt b = match b.bstmts with
   | [] ->
     (match stmt.skind with

src/plugins/e-acsl/src/code_generator/smart_stmt.mli

@@ -40,18 +40,28 @@ val block_from_stmts: stmt list -> stmt
 (** Create a block statement from a statement list. *)
 
 val assigns: loc:location -> result:lval -> exp -> stmt
-(** [assigns ~loc ~result value] create a statement to assign the [value]
+(** [assigns ~loc ~result value] creates a statement to assign the [value]
     expression to the [result] lval. *)
 
+val assigns_field: loc:location -> varinfo -> string -> exp -> stmt
+(** [assigns_field ~loc vi field value] creates a statement to assign the
+    [value] expression to the [field] of the structure in the variable [vi]. *)
+
 val if_stmt:
   loc:location -> cond:exp -> ?else_blk:block -> block -> stmt
-(** [if ~loc ~cond ~then_blk ~else_blk] create an if statement with [cond]
+(** [if ~loc ~cond ~then_blk ~else_blk] creates an if statement with [cond]
     as condition and [then_blk] and [else_blk] as respectively "then" block and
     "else" block. *)
 
 val break: loc:location -> stmt
 (** Create a break statement *)
 
+val struct_local_init: loc:location -> varinfo -> (string * exp) list -> stmt
+(** [struct_local_init ~loc vi fields] creates a local initialization for the
+    structure variable [vi]. [fields] is a list of couple [(name, e)] where
+    [name] is the name of a field in the structure and [e] is the expression to
+    initialize that field. *)
+
 (* ********************************************************************** *)
 (* E-ACSL specific code: build calls to its RTL API *)
 (* ********************************************************************** *)