diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-18 19:52:27 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-18 19:52:27 +0200 |
| commit | 74d06cfedc4a57fbb0be8772431033120b553ab2 (patch) | |
| tree | e923f3bd697e21d75a45885fe6b482d4571a9e5e /arm/ValueAOp.v | |
| parent | f440208c6b6159fd83dd6c365e194fe39b30d794 (diff) | |
| download | compcert-kvx-74d06cfedc4a57fbb0be8772431033120b553ab2.tar.gz compcert-kvx-74d06cfedc4a57fbb0be8772431033120b553ab2.zip | |
ValueDomain.aptr_of_aval: be more conservative with pointers synthesized from numbers.
For example: *((int *) 0x10000) = 0. This write used to be treated as not interfering with any load. With this change, in relaxed value analysis mode, it is treated as interfering with any load except those from the current stack frame.
Diffstat (limited to 'arm/ValueAOp.v')
0 files changed, 0 insertions, 0 deletions