sig
exception NotACType
type ('value, 'shape) typ
val of_ltyp : Cil_types.logic_type -> (unit, unit) typ
val integer : (unit, unit) typ
val real : (unit, unit) typ
val of_ctyp : Cil_types.typ -> ('v, 'v) 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 int : ('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 attribute :
('v, 's) typ -> string -> Cil_types.attrparam list -> ('v, 's) typ
val const : ('v, 's) typ -> ('v, 's) typ
val stdlib_generated : ('v, 's) typ -> ('v, 's) typ
val cil_typ : ('v, 's) typ -> Cil_types.typ
val cil_logic_type : ('v, 's) typ -> Cil_types.logic_type
type const'
type var'
type lval'
type exp'
type init'
type label
type const = [ `const of Cil_builder.Exp.const' ]
type var = [ `var of Cil_builder.Exp.var' ]
type lval =
[ `lval of Cil_builder.Exp.lval' | `var of Cil_builder.Exp.var' ]
type exp =
[ `const of Cil_builder.Exp.const'
| `exp of Cil_builder.Exp.exp'
| `lval of Cil_builder.Exp.lval'
| `var of Cil_builder.Exp.var' ]
type init =
[ `const of Cil_builder.Exp.const'
| `exp of Cil_builder.Exp.exp'
| `init of Cil_builder.Exp.init'
| `lval of Cil_builder.Exp.lval'
| `var of Cil_builder.Exp.var' ]
val pretty :
Stdlib.Format.formatter ->
[ `const of Cil_builder.Exp.const'
| `exp of Cil_builder.Exp.exp'
| `init of Cil_builder.Exp.init'
| `lval of Cil_builder.Exp.lval'
| `none
| `var of Cil_builder.Exp.var' ] -> unit
val none : [> `none ]
val here : Cil_builder.Exp.label
val old : Cil_builder.Exp.label
val pre : Cil_builder.Exp.label
val post : Cil_builder.Exp.label
val loop_entry : Cil_builder.Exp.label
val loop_current : Cil_builder.Exp.label
val program_init : Cil_builder.Exp.label
val of_constant : Cil_types.constant -> [> Cil_builder.Exp.const ]
val of_int : int -> [> Cil_builder.Exp.const ]
val of_integer : Integer.t -> [> Cil_builder.Exp.const ]
val zero : [> Cil_builder.Exp.const ]
val one : [> Cil_builder.Exp.const ]
val var : Cil_types.varinfo -> [> Cil_builder.Exp.var ]
val of_lval : Cil_types.lval -> [> Cil_builder.Exp.lval ]
exception EmptyList
val of_exp : Cil_types.exp -> [> Cil_builder.Exp.exp ]
val of_exp_copy : Cil_types.exp -> [> Cil_builder.Exp.exp ]
val unop :
Cil_types.unop -> [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val neg : [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val lognot : [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val bwnot : [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val succ : [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val add_int : [< Cil_builder.Exp.exp ] -> int -> [> Cil_builder.Exp.exp ]
val binop :
Cil_types.binop ->
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val add :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val sub :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val mul :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val div :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val modulo :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val shiftl :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val shiftr :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val lt :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val gt :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val le :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val ge :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val eq :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val ne :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val logor :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val logand :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val logor_list : [< Cil_builder.Exp.exp ] list -> Cil_builder.Exp.exp
val logand_list : [< Cil_builder.Exp.exp ] list -> Cil_builder.Exp.exp
val bwand :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val bwor :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val bwxor :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val cast :
('v, 's) typ -> [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val cast' :
Cil_types.typ -> [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val addr : [< Cil_builder.Exp.lval ] -> [> Cil_builder.Exp.exp ]
val mem : [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.lval ]
val index :
[< Cil_builder.Exp.lval ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.lval ]
val field :
[< Cil_builder.Exp.lval ] ->
Cil_types.fieldinfo -> [> Cil_builder.Exp.lval ]
val fieldnamed :
[< Cil_builder.Exp.lval ] -> string -> [> Cil_builder.Exp.lval ]
val result : [> Cil_builder.Exp.lval ]
val term : Cil_types.term -> [> Cil_builder.Exp.exp ]
val range :
[< `const of Cil_builder.Exp.const'
| `exp of Cil_builder.Exp.exp'
| `lval of Cil_builder.Exp.lval'
| `none
| `var of Cil_builder.Exp.var' ] ->
[< `const of Cil_builder.Exp.const'
| `exp of Cil_builder.Exp.exp'
| `lval of Cil_builder.Exp.lval'
| `none
| `var of Cil_builder.Exp.var' ] ->
[> Cil_builder.Exp.exp ]
val whole : [> Cil_builder.Exp.exp ]
val whole_right : [> Cil_builder.Exp.exp ]
val app :
Cil_types.logic_info ->
Cil_builder.Exp.label list ->
[< Cil_builder.Exp.exp ] list -> [> Cil_builder.Exp.exp ]
val object_pointer :
?at:Cil_builder.Exp.label ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val valid :
?at:Cil_builder.Exp.label ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val valid_read :
?at:Cil_builder.Exp.label ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val initialized :
?at:Cil_builder.Exp.label ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val dangling :
?at:Cil_builder.Exp.label ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val allocable :
?at:Cil_builder.Exp.label ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val freeable :
?at:Cil_builder.Exp.label ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val fresh :
Cil_builder.Exp.label ->
Cil_builder.Exp.label ->
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val of_init : Cil_types.init -> [> Cil_builder.Exp.init ]
val compound :
Cil_types.typ -> Cil_builder.Exp.init list -> [> Cil_builder.Exp.init ]
val values :
(Cil_builder.Exp.init, 'values) typ -> 'values -> Cil_builder.Exp.init
val ( + ) :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val ( - ) :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val ( * ) :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val ( / ) :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val ( % ) :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val ( << ) :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val ( >> ) :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val ( < ) :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val ( > ) :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val ( <= ) :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val ( >= ) :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val ( == ) :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val ( != ) :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
val ( -- ) :
[< Cil_builder.Exp.exp ] ->
[< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
exception LogicInC of Cil_builder.Exp.exp
exception CInLogic of Cil_builder.Exp.exp
exception NotATerm of Cil_builder.Exp.exp
exception NotAPredicate of Cil_builder.Exp.exp
exception NotAFunction of Cil_types.logic_info
exception Typing_error of string
val cil_logic_label : Cil_builder.Exp.label -> Cil_types.logic_label
val cil_constant : [< Cil_builder.Exp.const ] -> Cil_types.constant
val cil_varinfo : [< Cil_builder.Exp.var ] -> Cil_types.varinfo
val cil_lval :
loc:Cil_types.location -> [< Cil_builder.Exp.lval ] -> Cil_types.lval
val cil_exp :
loc:Cil_types.location -> [< Cil_builder.Exp.exp ] -> Cil_types.exp
val cil_term_lval :
loc:Cil_types.location ->
?restyp:Cil_types.typ -> [< Cil_builder.Exp.lval ] -> Cil_types.term_lval
val cil_term :
loc:Cil_types.location ->
?restyp:Cil_types.typ -> [< Cil_builder.Exp.exp ] -> Cil_types.term
val cil_iterm :
loc:Cil_types.location ->
?restyp:Cil_types.typ ->
[< Cil_builder.Exp.exp ] -> Cil_types.identified_term
val cil_pred :
loc:Cil_types.location ->
?restyp:Cil_types.typ -> [< Cil_builder.Exp.exp ] -> Cil_types.predicate
val cil_ipred :
loc:Cil_types.location ->
?restyp:Cil_types.typ ->
[< Cil_builder.Exp.exp ] -> Cil_types.identified_predicate
val cil_init :
loc:Cil_types.location -> [< Cil_builder.Exp.init ] -> Cil_types.init
val cil_typeof : [< Cil_builder.Exp.var ] -> Cil_types.typ
end