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