Frama-C API - Make_Narrow
Parameters
module _ : sig ... end
Signature
Over-approximation of the intersection of abstract values, without considering (bitwise) reinterpretations. In particular, values with equivalent representations (e.g. -1
and 0xFF
on 8 bits) may be considered different, leading to empty intersections. This may result in unsound results; the function narrow_reinterpret
below should be preferred in general.