Module Cil_builder.Stateful
Parameters
Signature
include module type of Exp
with type ('v, 's) typ = ( 'v, 's ) Type.typ
and type const' = Exp.const'
and type var' = Exp.var'
and type lval' = Exp.lval'
and type exp' = Exp.exp'
and type init' = Exp.init'
and type label = Exp.label
include module type of Type with type ('v, 's) typ = ( 'v, 's ) Type.typ
val integer : ( unit, unit ) typ
val real : ( unit, unit ) typ
val void : ( 'v, 'v ) typ
val bool : ( 'v, 'v ) typ
val char : ( 'v, 'v ) typ
val schar : ( 'v, 'v ) typ
val uchar : ( 'v, 'v ) typ
val unit : ( 'v, 'v ) typ
val short : ( 'v, 'v ) typ
val ushort : ( 'v, 'v ) typ
val long : ( 'v, 'v ) typ
val ulong : ( 'v, 'v ) typ
val longlong : ( 'v, 'v ) typ
val ulonglong : ( 'v, 'v ) typ
val float : ( 'v, 'v ) typ
val double : ( 'v, 'v ) typ
val longdouble : ( 'v, 'v ) typ
val ptr : ( 'v, 's ) typ -> ( 'v, 'v ) typ
val array : ?size:int -> ( 'v, 's ) typ -> ( 'v, 's list ) typ
val const : ( 'v, 's ) typ -> ( 'v, 's ) typ
val stdlib_generated : ( 'v, 's ) typ -> ( 'v, 's ) typ
val pretty : Stdlib.Format.formatter -> [ init | `none ] -> unit
val of_int : int -> [> const ]
val neg : [< exp ] -> [> exp ]
val lognot : [< exp ] -> [> exp ]
val bwnot : [< exp ] -> [> exp ]
val succ : [< exp ] -> [> exp ]
val add_int : [< exp ] -> int -> [> exp ]
val modulo : [< exp ] -> [< exp ] -> [> exp ]
val shiftl : [< exp ] -> [< exp ] -> [> exp ]
val shiftr : [< exp ] -> [< exp ] -> [> exp ]
val logand : [< exp ] -> [< exp ] -> [> exp ]
val logor_list : [< exp ] list -> exp
val logand_list : [< exp ] list -> exp
val cast : ( 'v, 's ) typ -> [< exp ] -> [> exp ]
val fieldnamed : [< lval ] -> string -> [> lval ]
val range : [< exp | `none ] -> [< exp | `none ] -> [> exp ]
val whole_right : [> exp ]
exception LogicInC of exp
exception CInLogic of exp
exception NotATerm of exp
exception NotAPredicate of exp
exception Typing_error of string
exception OutOfScope of string
val set_return_type : ( 's, 'v ) typ -> unit
val add_stdlib_generated : unit -> unit
val assigns : [< exp ] list -> [< exp | `indirect of [< exp ] ] list -> unit
val requires : [< exp ] -> unit
val ensures : [< exp ] -> unit
val open_else : ?ghost:bool -> unit -> unit
val case : [< exp ] -> unit
val return : [< exp | `none ] -> unit
val local : ?ghost:bool -> ?init:'v -> ( init, 'v ) typ -> string -> [> var ]
val local_copy : ?ghost:bool -> ?suffix:string -> [< var ] -> [> var ]
val assign : [< lval ] -> [< exp ] -> unit
val incr : [< lval ] -> unit
val call : [< lval | `none ] -> [< exp ] -> [< exp ] list -> unit
val pure : [< exp ] -> unit
val (:=) : [< lval ] -> [< exp ] -> unit
val (+=) : [< lval ] -> [< exp ] -> unit
val (-=) : [< lval ] -> [< exp ] -> unit