module Eval_op: sig
.. end
Numeric evaluation. Factored with evaluation in the logic.
val pp_v : Cvalue.V.t -> Format.formatter -> unit
val offsetmap_of_v : typ:Cil_types.typ -> Cvalue.V.t -> Cvalue.V_Offsetmap.t
Transformation a value into an offsetmap of size sizeof(typ)
bytes.
val wrap_int : Cvalue.V.t -> Cvalue.V_Offsetmap.t option
Specialization of the function above for standard types
val wrap_ptr : Cvalue.V.t -> Cvalue.V_Offsetmap.t option
val wrap_double : Cvalue.V.t -> Cvalue.V_Offsetmap.t option
val is_bitfield : Cil_types.typ -> bool
Bitfields
val sizeof_lval_typ : Cil_types.typ -> Int_Base.t
Size of the type of a lval, taking into account that the lval might have
been a bitfield.
val cast_lval_bitfield : Cil_types.typ -> Int_Base.i -> Cvalue.V.t -> Cvalue.V.t
val reinterpret_int : with_alarms:CilE.warn_mode -> Cil_types.ikind -> Cvalue.V.t -> Cvalue.V.t
Read the given value value as an int of the given ikind
. Warn if the
value contains an address.
val reinterpret_float : with_alarms:CilE.warn_mode -> Cil_types.fkind -> Cvalue.V.t -> Cvalue.V.t
Read the given value value as a float int of the given fkind
. Warn if the
value contains an address, or is not representable as a finite float.
val reinterpret : with_alarms:CilE.warn_mode -> Cil_types.typ -> Cvalue.V.t -> Cvalue.V.t
val v_uninit_of_offsetmap : with_alarms:CilE.warn_mode ->
typ:Cil_types.typ -> Cvalue.V_Offsetmap.t -> Cvalue.V_Offsetmap.v
Reads the contents of the offsetmap (assuming it contains sizeof(typ)
bytes), and return them as an uninterpreted value.
val v_of_offsetmap : with_alarms:CilE.warn_mode ->
typ:Cil_types.typ -> Cvalue.V_Offsetmap.t -> Cvalue.V.t
Reads the contents of the offsetmap (assuming it contains sizeof(typ)
bytes) as a value of type V.t, then convert the result to type typ
val do_promotion : with_alarms:CilE.warn_mode ->
Ival.Float_abstract.rounding_mode ->
src_typ:Cil_types.typ ->
dst_typ:Cil_types.typ ->
Cvalue.V.t -> (Format.formatter -> unit) -> Cvalue.V.t
val handle_overflow : with_alarms:CilE.warn_mode ->
warn_unsigned:bool -> Cil_types.typ -> Cvalue.V.t -> Cvalue.V.t
val eval_binop_float : with_alarms:CilE.warn_mode ->
Ival.Float_abstract.rounding_mode ->
Cil_types.fkind option ->
Cvalue.V.t -> Cil_types.binop -> Cvalue.V.t -> Cvalue.V.t
val eval_binop_int : with_alarms:CilE.warn_mode ->
?typ:Cil_types.typ ->
te1:Cil_types.typ ->
Cvalue.V.t -> Cil_types.binop -> Cvalue.V.t -> Cvalue.V.t
val eval_uneg : with_alarms:CilE.warn_mode -> Cvalue.V.t -> Cil_types.typ -> Cvalue.V.t
val eval_unop : check_overflow:bool ->
with_alarms:CilE.warn_mode ->
Cvalue.V.t -> Cil_types.typ -> Cil_types.unop -> Cvalue.V.t
val reduce_rel_symmetric_int : bool -> Cil_types.binop -> Cvalue.V.t -> Cvalue.V.t -> Cvalue.V.t
val reduce_rel_symmetric_float : bool -> Cil_types.binop -> Cvalue.V.t -> Cvalue.V.t -> Cvalue.V.t
val reduce_rel_antisymmetric_int : typ_loc:'a ->
bool -> Cil_types.binop -> Cvalue.V.t -> Cvalue.V.t -> Cvalue.V.t
val reduce_rel_antisymmetric_float : bool ->
typ_loc:Cil_types.typ ->
bool -> Cil_types.binop -> Cvalue.V.t -> Cvalue.V.t -> Cvalue.V.t
type
reduce_rel_int_float = {
}
val reduce_rel_int : reduce_rel_int_float
val reduce_rel_float : bool -> reduce_rel_int_float
val eval_float_constant : with_alarms:CilE.warn_mode ->
float -> Cil_types.fkind -> string option -> Cvalue.V.t
The arguments are the approximate float value computed during parsing, the
size of the floating-point type, and the string representing the initial
constant if available. Return an abstract value that may be bottom if the
constant is outside of the representable range, or that may be imprecise
if it is not exactly representable.
val light_topify : Cvalue.V.z -> Cvalue.V.z
Change all offsets to top_int. Currently used to approximate volatile
values.