Module Cvalue_backward

module Cvalue_backward: sig .. end
Abstract reductions on Cvalue.V.t


See ! for details about backward operations.
val backward_binop : typ_res:Cil_types.typ ->
res_value:Cvalue.V.t ->
typ_e1:Cil_types.typ ->
Cvalue.V.t ->
Cil_types.binop -> Cvalue.V.t -> (Cvalue.V.t * Cvalue.V.t) option
This 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:Cil_types.typ ->
Cil_types.unop -> arg:Cvalue.V.t -> res:Cvalue.V.t -> Cvalue.V.t option
This 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:Cil_types.typ ->
dst_typ:Cil_types.typ ->
src_val:Cvalue.V.t -> dst_val:Cvalue.V.t -> Cvalue.V.t option
This 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.