From 615d6ca04e60cb760b7da9618a1f059d718fd4cf Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 19 Jul 2021 14:30:17 +0200
Subject: [PATCH] [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.
---
.../e-acsl/src/code_generator/smart_stmt.ml | 50 +++++++++++++++++++
.../e-acsl/src/code_generator/smart_stmt.mli | 14 +++++-
2 files changed, 62 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
index 03c60a57aaa..12a62406018 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
index ddf4f39ee60..c9aa2faad52 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
+++ b/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 *)
(* ********************************************************************** *)
--
GitLab