Frama-C API - Cvalue_backward
Abstract reductions on Cvalue.V.t
See Abstract_value for details about backward operations.
val backward_binop : typ_res:Frama_c_kernel.Cil_types.typ -> res_value:Frama_c_kernel.Cvalue.V.t -> typ_e1: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.t * Frama_c_kernel.Cvalue.V.t) optionThis function tries to reduce the argument values of a binary operation, given its result. typ_res is a type of res_value, and typ_e1 the type of v1.
val backward_unop : typ_arg:Frama_c_kernel.Cil_types.typ -> Eva_ast.unop -> arg:Frama_c_kernel.Cvalue.V.t -> res:Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.t optionThis function tries to reduce the argument value of an unary operation, given its result. typ_arg is the type of arg.
val backward_cast : src_typ:Frama_c_kernel.Cil_types.typ -> dst_typ:Frama_c_kernel.Cil_types.typ -> src_val:Frama_c_kernel.Cvalue.V.t -> dst_val:Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.t optionThis function tries to reduce the argument of a cast, given the result of the cast. src_typ is the type of src_val, dst_typ the type of the cast and of dst_val. Returning None means that not reduction was possible. Remember that the engine will intersect the result with src_val, no need to do this ourself.