[Cil builder] Implements some statements generation for Pure builder

src/kernel_services/ast_building/cil_builder.mli

@@ -204,6 +204,7 @@ sig
   exception NotAPredicate of exp
   exception NotAFunction of Cil_types.logic_info
   exception Typing_error of string
+  exception OutOfScope of string
 
   val cil_logic_label : label -> Cil_types.logic_label
   val cil_constant : [< const] -> Cil_types.constant
@@ -245,18 +246,37 @@ sig
   val incr : [< lval] -> [> instr]
   val call : [< lval | `none] -> [< exp] -> [< exp] list -> [> instr]
 
+  val local : ?ghost:bool -> ?init:'v -> (init,'v) typ -> string ->
+    [> var] * [> instr]
+  val local' : ?ghost:bool -> ?init:init -> Cil_types.typ -> string ->
+    [> var] * [> instr]
+  val local_copy : ?ghost:bool -> ?suffix:string -> [< var] ->
+    [> var] * [> instr]
+
   (* Statements *)
   val of_stmtkind : Cil_types.stmtkind -> [> stmt]
   val of_stmt : Cil_types.stmt -> [> stmt]
   val of_stmts : Cil_types.stmt list -> [> stmt]
   val block : [< stmt] list -> [> stmt]
+  val sequence : [< stmt] list -> [> stmt] (* does not generate block *)
   val ghost : [< stmt] -> [> stmt]
+  val if_ : [< exp] -> then_:[< stmt] list -> else_:[< stmt] list -> [> stmt]
+
+  (* Conversion to Cil *)
 
-  val cil_instr : loc:Cil_types.location -> instr -> Cil_types.instr
-  val cil_stmtkind : loc:Cil_types.location -> stmt -> Cil_types.stmtkind
-  val cil_stmt : loc:Cil_types.location -> stmt -> Cil_types.stmt
+  (* for the three following function into is mandatory if the built ast
+     contains locals declarations *)
+  val cil_instr : ?into:Cil_types.fundec ->
+    loc:Cil_types.location -> instr -> Cil_types.instr
+  val cil_stmtkind : ?into:Cil_types.fundec ->
+    loc:Cil_types.location -> stmt -> Cil_types.stmtkind
+  val cil_stmt : ?into:Cil_types.fundec ->
+    loc:Cil_types.location -> stmt -> Cil_types.stmt
 
   (* Operators *)
+  val (let+) : var * stmt -> (var -> stmt list) -> stmt list
+  val (and+) : var -> var -> var * var
+
   val (:=) : [< lval] -> [< exp] -> [> instr] (* assign *)
   val (+=) : [< lval] -> [< exp] -> [> instr]
   val (-=) : [< lval] -> [< exp] -> [> instr]
@@ -342,4 +362,3 @@ sig
   val (+=) : [< lval] -> [< exp] -> unit
   val (-=) : [< lval] -> [< exp] -> unit
 end
-

tests/misc/cil_builder.i

+/* run.config
+MODULE: @PTEST_NAME@
+  OPT:
+*/
+
+void main(void) {
+    // This will be filled by the OCaml Module
+}

tests/misc/cil_builder.ml

+module Build = Cil_builder.Pure
+
+let run () =
+  let kf, _ = Globals.entry_point () in
+  let stmt = Kernel_function.find_first_stmt kf in
+  let loc = Kernel_function.get_location kf in
+  let into = Kernel_function.get_definition kf in
+  stmt.skind <- Build.(
+      cil_stmtkind ~into ~loc @@ sequence @@
+      let+ i = local int "x" in [
+        i := (of_int 1);
+        if_ (i < of_int 3)
+          ~then_:[incr i]
+          ~else_:[i := zero]
+      ]
+    );
+  Kernel.result "%a" Printer.pp_file (Ast.get ())
+
+
+let () =
+  Db.Main.extend run

tests/misc/oracle/cil_builder.res.oracle

+[kernel] Parsing cil_builder.i (no preprocessing)
+[kernel] /* Generated by Frama-C */
+  void main(void)
+  {
+    {
+      int x;
+      x = 1;
+      if (x < 3) x ++; else x = 0;
+    }
+  }