sig
  val stmt : Cil_types.stmtkind -> Cil_types.stmt
  val block : Cil_types.stmt -> Cil_types.block -> Cil_types.stmt
  val block_stmt : Cil_types.block -> Cil_types.stmt
  val block_from_stmts : Cil_types.stmt list -> Cil_types.stmt
  val assigns :
    loc:Cil_types.location ->
    result:Cil_types.lval -> Cil_types.exp -> Cil_types.stmt
  val if_stmt :
    loc:Cil_types.location ->
    cond:Cil_types.exp ->
    ?else_blk:Cil_types.block -> Cil_types.block -> Cil_types.stmt
  val break : loc:Cil_types.location -> Cil_types.stmt
  val lib_call :
    loc:Cil_types.location ->
    ?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
  val rtl_call :
    loc:Cil_types.location ->
    ?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
  val store_stmt :
    ?str_size:Cil_types.exp -> Cil_types.varinfo -> Cil_types.stmt
  val duplicate_store_stmt :
    ?str_size:Cil_types.exp -> Cil_types.varinfo -> Cil_types.stmt
  val delete_stmt : ?is_addr:bool -> Cil_types.varinfo -> Cil_types.stmt
  val full_init_stmt : Cil_types.varinfo -> Cil_types.stmt
  val initialize : loc:Cil_types.location -> Cil_types.lval -> Cil_types.stmt
  val mark_readonly : Cil_types.varinfo -> Cil_types.stmt
  type annotation_kind =
      Assertion
    | Precondition
    | Postcondition
    | Invariant
    | RTE
  val runtime_check :
    Smart_stmt.annotation_kind ->
    Cil_types.kernel_function ->
    Cil_types.exp -> Cil_types.predicate -> Cil_types.stmt
  val runtime_check_with_msg :
    loc:Cil_types.location ->
    string ->
    Smart_stmt.annotation_kind ->
    Cil_types.kernel_function -> Cil_types.exp -> Cil_types.stmt
end