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
. 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.