Frama-C API - Cvalue_forward
Forward operations on Cvalue.V.t
val are_comparable : Frama_c_kernel.Abstract_interp.Comp.t -> Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.t -> boolSubtype of Abstract_value.truth.
val assume_non_zero : Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.t truthval assume_bounded : Abstract_value.bound_kind -> Abstract_value.bound -> Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.t truthval assume_not_nan : assume_finite:bool -> Frama_c_kernel.Cil_types.fkind -> Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.t truthval assume_pointer : Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.t truthval assume_aligned : int -> Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.t truthval assume_comparable : Abstract_value.pointer_comparison -> Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.t -> (Frama_c_kernel.Cvalue.V.t * Frama_c_kernel.Cvalue.V.t) truthval forward_binop_int : typ:Frama_c_kernel.Cil_types.typ -> Frama_c_kernel.Cvalue.V.t -> Eva_ast.binop -> Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.tval forward_binop_float : Frama_c_kernel.Fval.kind -> Frama_c_kernel.Cvalue.V.t -> Eva_ast.binop -> Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.tval forward_unop : Frama_c_kernel.Cil_types.typ -> Eva_ast.unop -> Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.tval rewrap_integer : Eval_typ.integer_range -> Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.tval reinterpret : Frama_c_kernel.Cil_types.typ -> Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.tval cast_float_to_int : Eval_typ.integer_range -> Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.tval forward_cast : src_type:Eval_typ.scalar_typ -> dst_type:Eval_typ.scalar_typ -> Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.tval make_volatile : ?typ:Frama_c_kernel.Cil_types.typ -> Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.tmake_volatile ?typ v makes the value v more general (to account for external modifications), whenever typ is None or when it has type qualifier volatile.
val eval_float_constant : float -> Frama_c_kernel.Cil_types.fkind -> string option -> Frama_c_kernel.Cvalue.V.t