Frama-C API - Make_Narrow

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. Requires both offsetmaps to cover the same range; fails otherwise.

Variant of the function above that bitwise-reinterprets values before performing the intersection (in order to get normal forms). This may lead to situations where the result is not included in the arguments, but this function should be preferred to narrow. Requires both offsetmaps to cover the same range; fails otherwise.