diff --git a/src/plugins/e-acsl/src/code_generator/constructor.ml b/src/plugins/e-acsl/src/code_generator/constructor.ml index eb010f92eb65a2cf9cacdd39a3e5ea53a47dd8d4..4848a1f2e2191770084af933d615f5326926c81c 100644 --- a/src/plugins/e-acsl/src/code_generator/constructor.ml +++ b/src/plugins/e-acsl/src/code_generator/constructor.ml @@ -26,7 +26,31 @@ open Cil_types (* Expressions *) (* ********************************************************************** *) -let mk_deref ~loc lv = Cil.new_exp ~loc (Lval(Mem(lv), NoOffset)) +let extract_uncoerced_lval e = + let rec aux e = + match e.enode with + | Lval _ -> Some e + | CastE (_, e) -> aux e + | _ -> None + in + aux e + +let mk_lval ~loc lval = + Cil.new_exp ~loc (Lval lval) + +let mk_deref ~loc lv = mk_lval ~loc (Mem lv, NoOffset) + +let mk_subscript ~loc array idx = + match extract_uncoerced_lval array with + | Some { enode = Lval lval } -> + let subscript_lval = Cil.addOffsetLval (Index(idx, NoOffset)) lval in + mk_lval ~loc subscript_lval + | Some _ | None -> + Options.fatal + ~current:true + "Trying to create a subscript on an array that is not an Lval: %a" + Cil_types_debug.pp_exp + array (* ********************************************************************** *) (* Statements *) @@ -34,8 +58,16 @@ let mk_deref ~loc lv = Cil.new_exp ~loc (Lval(Mem(lv), NoOffset)) let mk_stmt sk = Cil.mkStmt ~valid_sid:true sk let mk_instr i = mk_stmt (Instr i) +let mk_block_stmt blk = mk_stmt (Block blk) let mk_call ~loc ?result e args = mk_instr (Call(result, e, args, loc)) +let mk_assigns ~loc ~result e = mk_instr (Set(result, e, loc)) + +let mk_if ~loc ~cond ?(else_blk=Cil.mkBlock []) then_blk = + mk_stmt (If (cond, then_blk, else_blk, loc)) + +let mk_break ~loc = mk_stmt (Break loc) + type annotation_kind = | Assertion | Precondition @@ -59,7 +91,7 @@ let mk_block stmt b = match b.bstmts with | Instr(Skip _) -> stmt | _ -> assert false) | [ s ] -> s - | _ :: _ -> mk_stmt (Block b) + | _ :: _ -> mk_block_stmt b (* ********************************************************************** *) (* E-ACSL specific code *) diff --git a/src/plugins/e-acsl/src/code_generator/constructor.mli b/src/plugins/e-acsl/src/code_generator/constructor.mli index 676bfe14af6286cc19179f2d0c8c0aa1a6badc4e..731734839878fda808895f9a71e4fde5858f4d4c 100644 --- a/src/plugins/e-acsl/src/code_generator/constructor.mli +++ b/src/plugins/e-acsl/src/code_generator/constructor.mli @@ -25,13 +25,54 @@ open Cil_types open Cil_datatype +(* ********************************************************************** *) +(* Expressions *) +(* ********************************************************************** *) + +val extract_uncoerced_lval: exp -> exp option +(** Unroll the [CastE] part of the expression until an [Lval] is found, and + return it. + + If at some point the expression is neither a [CastE] nor an [Lval], then + return [None]. *) + +val mk_lval: loc:location -> lval -> exp +(** Construct an lval expression from an lval. *) + val mk_deref: loc:Location.t -> exp -> exp (** Construct a dereference of an expression. *) +val mk_subscript: loc:location -> exp -> exp -> exp +(** [mk_subscript ~loc array idx] Create an expression to access the [idx]'th + element of the [array]. *) + +(* ********************************************************************** *) +(* Statements *) +(* ********************************************************************** *) + +val mk_stmt: stmtkind -> stmt +(** Create a statement from a statement kind. *) + val mk_block: stmt -> block -> stmt (** Create a block statement from a block to replace a given statement. Requires that (1) the block is not empty, or (2) the statement is a skip. *) +val mk_block_stmt: block -> stmt +(** Create a block statement from a block *) + +val mk_assigns: loc:location -> result:lval -> exp -> stmt +(** [mk_assigns ~loc ~result value] create a statement to assign the [value] + expression to the [result] lval. *) + +val mk_if: + loc:location -> cond:exp -> ?else_blk:block -> block -> stmt +(** [mk_if ~loc ~cond ~then_blk ~else_blk] create an if statement with [cond] + as condition and [then_blk] and [else_blk] as respectively "then" block and + "else" block. *) + +val mk_break: loc:location -> stmt +(** Create a break statement *) + (* ********************************************************************** *) (* E-ACSL specific code: build calls to its RTL API *) (* ********************************************************************** *)