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