diff --git a/src/kernel_services/ast_building/cil_builder.ml b/src/kernel_services/ast_building/cil_builder.ml
index 62e90943b9eb30621cf58f479633bc13f5c0ea0d..c59609f5aa9536d2b996066c580f36e2f9f93b2d 100644
--- a/src/kernel_services/ast_building/cil_builder.ml
+++ b/src/kernel_services/ast_building/cil_builder.ml
@@ -537,11 +537,84 @@ struct
let loc = Location.loc
+
+ (* Conversion to Cil *)
+
+ let build_instr_list l =
+ let rev_build_one acc = function
+ | Label _ | CilStmt _ | CilStmtkind _ ->
+ raise (WrongContext "not convertible to instr")
+ | CilInstr instr -> instr :: acc
+ in
+ List.fold_left rev_build_one [] l
+
+ let build_stmt_list ~ghost l =
+ let rev_build_one acc = function
+ | Label l ->
+ begin match acc with
+ | [] -> (* No generated statement to attach the label to *)
+ let stmt = Cil.mkEmptyStmt ~ghost ~loc () in
+ stmt.Cil_types.labels <- [l];
+ stmt :: acc
+ | stmt :: _ -> (* There is a statement to attach the label to *)
+ stmt.Cil_types.labels <- l :: stmt.Cil_types.labels;
+ acc
+ end
+ | CilStmt stmt ->
+ stmt :: acc
+ | CilStmtkind sk ->
+ Cil.mkStmt ~ghost sk :: acc
+ | CilInstr instr ->
+ Cil.mkStmt ~ghost (Cil_types.Instr instr) :: acc
+ in
+ List.fold_left rev_build_one [] l
+
+ let build_block b =
+ let block = Cil.mkBlock (build_stmt_list ~ghost:b.ghost b.stmts) in
+ block.Cil_types.blocals <- List.rev b.vars;
+ block
+
+ let build_stmtkind b =
+ let block = build_block b in
+ match b.scope_type with
+ | Block ->
+ Cil_types.Block block
+ | IfThen { ifthen_exp } ->
+ Cil_types.If (ifthen_exp, block, Cil.mkBlock [], loc)
+ | IfThenElse { ifthenelse_exp; then_block } ->
+ Cil_types.If (ifthenelse_exp, then_block, block, loc)
+ | Switch { switch_exp } ->
+ let open Cil_types in
+ (* Case are only allowed in the current block by the case function *)
+ let contains_case stmt =
+ List.exists (function Case _ -> true | _ -> false) stmt.labels
+ in
+ let case_stmts = List.filter contains_case block.bstmts in
+ Cil_types.Switch (switch_exp, block, case_stmts , loc)
+ | Function _ ->
+ raise (WrongContext "not convertible to stmtkind")
+
+
(* State management *)
- let stack : scope list ref = ref []
let owner: Cil_types.fundec option ref = ref None
+ let reset_owner () =
+ owner := None
+
+ let set_owner o =
+ if Extlib.has_some !owner then
+ raise (WrongContext "already in a function");
+ owner := Some o
+
+ let get_owner () =
+ match !owner with
+ | None -> raise (WrongContext "function context not set")
+ | Some fundec -> fundec
+
+
+ let stack : scope list ref = ref []
+
let pretty_stack fmt =
let pretty_stack_type fmt b =
match b.scope_type with
@@ -584,72 +657,20 @@ struct
hd
let finish () =
+ reset_owner ();
match !stack with
| [] -> raise (WrongContext "not in an opened context")
| [b] -> b
| _ :: _ :: _ -> raise (WrongContext "all contextes have not been closed")
- let reset_owner () =
- owner := None
-
- let set_owner o =
- owner := Some o
-
- let get_owner () =
- match !owner with
- | None -> raise (WrongContext "not in an opened function")
- | Some fundec -> fundec
-
let append_stmt b s =
b.stmts <- s :: b.stmts
- (* Conversion to Cil *)
-
- let build_stmt_list ~ghost l =
- let rev_build_one acc = function
- | Label l ->
- begin match acc with
- | [] -> (* No generated statement to attach the label to *)
- let stmt = Cil.mkEmptyStmt ~ghost ~loc () in
- stmt.Cil_types.labels <- [l];
- stmt :: acc
- | stmt :: _ -> (* There is a statement to attach the label to *)
- stmt.Cil_types.labels <- l :: stmt.Cil_types.labels;
- acc
- end
- | CilStmt stmt ->
- stmt :: acc
- | CilStmtkind sk ->
- Cil.mkStmt ~ghost sk :: acc
- | CilInstr instr ->
- Cil.mkStmt ~ghost (Cil_types.Instr instr) :: acc
- in
- List.fold_left rev_build_one [] l
-
- let build_block b =
- let block = Cil.mkBlock (build_stmt_list ~ghost:b.ghost b.stmts) in
- block.Cil_types.blocals <- List.rev b.vars;
- block
+ let append_local v =
+ let fundec = get_owner () and b = top () in
+ fundec.Cil_types.slocals <- fundec.Cil_types.slocals @ [v];
+ b.vars <- v :: b.vars
- let build_stmtkind b =
- let block = build_block b in
- match b.scope_type with
- | Block ->
- Cil_types.Block block
- | IfThen { ifthen_exp } ->
- Cil_types.If (ifthen_exp, block, Cil.mkBlock [], loc)
- | IfThenElse { ifthenelse_exp; then_block } ->
- Cil_types.If (ifthenelse_exp, then_block, block, loc)
- | Switch { switch_exp } ->
- let open Cil_types in
- (* Case are only allowed in the current block by the case function *)
- let contains_case stmt =
- List.exists (function Case _ -> true | _ -> false) stmt.labels
- in
- let case_stmts = List.filter contains_case block.bstmts in
- Cil_types.Switch (switch_exp, block, case_stmts , loc)
- | Function _ ->
- raise (WrongContext "not convertible to stmtkind")
(* Statements *)
@@ -678,17 +699,20 @@ struct
push (new_block ?ghost (Function {fundec}));
`var fundec.Cil_types.svar
- let open_block () =
- push (new_block Block)
+ let open_block ?into ?ghost () =
+ Extlib.may set_owner into;
+ push (new_block ?ghost Block)
- let open_ghost () =
- push (new_block ~ghost:true Block)
+ let open_ghost ?into () =
+ open_block ?into ~ghost:true ()
- let open_switch exp =
+ let open_switch ?into exp =
+ Extlib.may set_owner into;
let switch_exp = cil_exp ~loc exp in
push (new_block (Switch {switch_exp}))
- let open_if exp =
+ let open_if ?into exp =
+ Extlib.may set_owner into;
let ifthen_exp = cil_exp ~loc exp in
push (new_block (IfThen {ifthen_exp}))
@@ -712,6 +736,17 @@ struct
| Cil_types.Block b -> b
| _ -> raise (WrongContext "not in an opened simple block context")
+ let finish_instr_list ?scope () =
+ let b = finish () in
+ begin match scope, b.vars with
+ | None, [] -> () (* Nothing to do *)
+ | Some block, vars ->
+ block.Cil_types.blocals <- List.rev vars @ block.Cil_types.blocals
+ | None, _ :: _ ->
+ raise (WrongContext "a scope must be provide to insert local variables")
+ end;
+ build_instr_list b.stmts
+
let finish_stmt () =
let b = finish () in
Cil.mkStmt ~ghost:b.ghost (build_stmtkind b)
@@ -731,7 +766,6 @@ struct
Cfg.prepareCFG ~keepSwitch fundec;
Cfg.cfgFun fundec;
end;
- reset_owner ();
GFun (fundec,loc)
| _ -> raise (WrongContext "not in a opened function context")
@@ -778,7 +812,7 @@ struct
let local' ?(ghost=false) ?init typ name =
let fundec = get_owner () and b = top () in
let ghost = ghost || b.ghost in
- let v = Cil.makeLocalVar fundec ~insert:false ~ghost ~loc name typ in
+ let v = Cil.makeLocalVar ~insert:false ~ghost ~loc fundec name typ in
begin match init with
| None -> ()
| Some init ->
@@ -786,6 +820,7 @@ struct
instr (Cil_types.Local_init (v, local_init, loc));
v.vdefined <- true
end;
+ append_local v;
`var v
let local ?ghost ?init typ name =
@@ -798,8 +833,7 @@ struct
let v = Cil.copyVarinfo vi (vi.Cil_types.vname ^ suffix) in
v.vghost <- v.vghost || ghost;
Cil.refresh_local_name fundec v;
- fundec.Cil_types.slocals <- fundec.Cil_types.slocals @ [v];
- b.vars <- v :: b.vars;
+ append_local v;
`var v
let parameter ?(ghost=false) ?(attributes=[]) typ name =
diff --git a/src/kernel_services/ast_building/cil_builder.mli b/src/kernel_services/ast_building/cil_builder.mli
index f6d22d45bc0fb504c4af8fcc0de6aeed0d8cd8eb..11c744096fa2deac101e03321673c94c8102fb49 100644
--- a/src/kernel_services/ast_building/cil_builder.mli
+++ b/src/kernel_services/ast_building/cil_builder.mli
@@ -229,13 +229,14 @@ sig
val stmt : Cil_types.stmt -> unit
val stmts : Cil_types.stmt list -> unit
val open_function : ?ghost:bool -> string -> [> var]
- val open_block : unit -> unit
- val open_ghost : unit -> unit
- val open_switch : [< exp] -> unit
- val open_if : [< exp] -> unit
+ val open_block : ?into:Cil_types.fundec -> ?ghost:bool -> unit -> unit
+ val open_ghost : ?into:Cil_types.fundec -> unit -> unit
+ val open_switch : ?into:Cil_types.fundec -> [< exp] -> unit
+ val open_if : ?into:Cil_types.fundec -> [< exp] -> unit
val open_else : unit -> unit
val close : unit -> unit
val finish_block : unit -> Cil_types.block
+ val finish_instr_list : ?scope:Cil_types.block -> unit -> Cil_types.instr list
val finish_stmt : unit -> Cil_types.stmt
val finish_function : ?register:bool -> unit -> Cil_types.global
val case : [< exp] -> unit