sig
type 'a or_bottom = [ `Bottom | `Value of 'a ]
val ( >>- ) : 'a or_bottom -> ('a -> 'b or_bottom) -> 'b or_bottom
val ( >>-: ) : 'a or_bottom -> ('a -> 'b) -> 'b or_bottom
type 'a or_top = [ `Top | `Value of 'a ]
type 't with_alarms = 't * Alarmset.t
type 't evaluated = 't or_bottom Eval.with_alarms
val ( >>= ) :
'a Eval.evaluated -> ('a -> 'b Eval.evaluated) -> 'b Eval.evaluated
val ( >>=. ) :
'a Eval.evaluated -> ('a -> 'b or_bottom) -> 'b Eval.evaluated
val ( >>=: ) : 'a Eval.evaluated -> ('a -> 'b) -> 'b Eval.evaluated
type 'a reduced = [ `Bottom | `Unreduced | `Value of 'a ]
type unop_context = { operand : Cil_types.exp; result : Cil_types.exp; }
type binop_context = {
left_operand : Cil_types.exp;
right_operand : Cil_types.exp;
binary_result : Cil_types.exp;
result_typ : Cil_types.typ;
}
type reductness = Unreduced | Reduced | Created | Dull
type 'a flagged_value = {
v : 'a or_bottom;
initialized : bool;
escaping : bool;
}
type ('a, 'origin) record_val = {
value : 'a Eval.flagged_value;
origin : 'origin option;
reductness : Eval.reductness;
val_alarms : Alarmset.t;
}
type 'a record_loc = {
loc : 'a;
typ : Cil_types.typ;
loc_alarms : Alarmset.t;
}
module type Valuation =
sig
type t
type value
type origin
type loc
val empty : Eval.Valuation.t
val find :
Eval.Valuation.t ->
Cil_types.exp ->
(Eval.Valuation.value, Eval.Valuation.origin) Eval.record_val
Eval.or_top
val add :
Eval.Valuation.t ->
Cil_types.exp ->
(Eval.Valuation.value, Eval.Valuation.origin) Eval.record_val ->
Eval.Valuation.t
val fold :
(Cil_types.exp ->
(Eval.Valuation.value, Eval.Valuation.origin) Eval.record_val ->
'a -> 'a) ->
Eval.Valuation.t -> 'a -> 'a
val find_loc :
Eval.Valuation.t ->
Cil_types.lval -> Eval.Valuation.loc Eval.record_loc Eval.or_top
val remove : Eval.Valuation.t -> Cil_types.exp -> Eval.Valuation.t
val remove_loc : Eval.Valuation.t -> Cil_types.lval -> Eval.Valuation.t
end
module Clear_Valuation :
functor (Valuation : Valuation) ->
sig
val clear_englobing_exprs :
Eval.Valuation.t ->
expr:Cil_types.exp -> subexpr:Cil_types.exp -> Eval.Valuation.t
end
type 'loc left_value = {
lval : Cil_types.lval;
lloc : 'loc;
ltyp : Cil_types.typ;
}
type 'value assigned =
Assign of 'value
| Copy of Cil_types.lval * 'value Eval.flagged_value
val value_assigned : 'value Eval.assigned -> 'value or_bottom
type 'value argument = {
formal : Cil_types.varinfo;
concrete : Cil_types.exp;
avalue : 'value Eval.assigned;
}
type 'value call = {
kf : Cil_types.kernel_function;
arguments : 'value Eval.argument list;
rest : (Cil_types.exp * 'value Eval.assigned) list;
return : Cil_types.varinfo option;
recursive : bool;
}
type 't init =
Default
| Continue of 't
| Custom of (Cil_types.stmt * 't) list
type 'state call_action =
Compute of 'state Eval.init * bool
| Result of 'state list or_bottom * Value_types.cacheable
exception InvalidCall
end