sig
  val mk_deref :
    loc:Cil_datatype.Location.t -> Cil_types.exp -> Cil_types.exp
  val mk_block : Cil_types.stmt -> Cil_types.block -> Cil_types.stmt
  val mk_lib_call :
    loc:Cil_datatype.Location.t ->
    ?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
  val mk_rtl_call :
    loc:Cil_datatype.Location.t ->
    ?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
  val mk_store_stmt :
    ?str_size:Cil_types.exp -> Cil_types.varinfo -> Cil_types.stmt
  val mk_duplicate_store_stmt :
    ?str_size:Cil_types.exp -> Cil_types.varinfo -> Cil_types.stmt
  val mk_delete_stmt : Cil_types.varinfo -> Cil_types.stmt
  val mk_full_init_stmt : ?addr:bool -> Cil_types.varinfo -> Cil_types.stmt
  val mk_initialize :
    loc:Cil_types.location -> Cil_types.lval -> Cil_types.stmt
  val mk_mark_readonly : Cil_types.varinfo -> Cil_types.stmt
  type annotation_kind =
      Assertion
    | Precondition
    | Postcondition
    | Invariant
    | RTE
  val mk_runtime_check :
    ?reverse:bool ->
    Constructor.annotation_kind ->
    Cil_types.kernel_function ->
    Cil_types.exp -> Cil_types.predicate -> Cil_types.stmt
end