From 8dc4d8e96858ca3deaea2a05ab83297af29c302f Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 22 Sep 2020 10:07:13 +0200
Subject: [PATCH] [eacsl:codegen] Create a helper function to build a block
statement from a list of statements
---
src/plugins/e-acsl/src/code_generator/smart_stmt.ml | 1 +
src/plugins/e-acsl/src/code_generator/smart_stmt.mli | 3 +++
2 files changed, 4 insertions(+)
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 dec6438762f..98418854690 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
@@ -29,6 +29,7 @@ open Cil_types
let stmt sk = Cil.mkStmt ~valid_sid:true sk
let instr i = stmt (Instr i)
let block_stmt blk = stmt (Block blk)
+let block_from_stmts stmts = block_stmt (Cil.mkBlock stmts)
let call ~loc ?result e args = instr (Call(result, e, args, loc))
let assigns ~loc ~result e = instr (Set(result, e, loc))
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 e0c919a7f88..3aebb9f4cc2 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
@@ -36,6 +36,9 @@ val block: stmt -> block -> stmt
val block_stmt: block -> stmt
(** Create a block statement from a block *)
+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]
expression to the [result] lval. *)
--
GitLab