diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-19 09:29:45 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-19 09:29:45 +0200 |
commit | 2932b531ceff2cd4573714aeaeb9b4e537d36af8 (patch) | |
tree | ed42351e245c076b8cd360d0e753e8c61090e8e5 /lib/Ordered.v | |
parent | 74d06cfedc4a57fbb0be8772431033120b553ab2 (diff) | |
download | compcert-2932b531ceff2cd4573714aeaeb9b4e537d36af8.tar.gz compcert-2932b531ceff2cd4573714aeaeb9b4e537d36af8.zip |
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.
Diffstat (limited to 'lib/Ordered.v')
0 files changed, 0 insertions, 0 deletions