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 dec6438762f3afb494812fa1799af9bb3557ebc6..984188546901494f65d6ab58fc6a88919f95dc49 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 e0c919a7f8847b7c23e71d536b619837ed59a2f5..3aebb9f4cc27419db8d9337096af57fb2d3cebb6 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. *)