Value analysis: keep track of pointer values that leak through arithmetic operations with undefined behaviors.

Consider (x ^ 1) ^ 1 where x is a intptr_t containing a pointer value.  "x ^ 1" evaluates to Vundef in the CompCert semantics, hence the value analysis, in strict mode, gives abstract result Ifptr Pbot (= any number but not a pointer).  In relaxed mode, we now give abstract result Ifptr (poffset p) where p is the abstraction of the pointer, thus keeping track of the actual leak of the pointer value.

0 files changed, 0 insertions, 0 deletions