diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-19 12:11:37 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-19 12:11:37 +0200 |
| commit | 78f1b6a57c95ecc68c104d4764fc8d5851d7dd54 (patch) | |
| tree | 0c39dadd44f196baa0835ba525e7fb4246ebee3d /backend/CSE.v | |
| parent | 2932b531ceff2cd4573714aeaeb9b4e537d36af8 (diff) | |
| download | compcert-kvx-78f1b6a57c95ecc68c104d4764fc8d5851d7dd54.tar.gz compcert-kvx-78f1b6a57c95ecc68c104d4764fc8d5851d7dd54.zip | |
Value analysis: keep track of pointer values that leak through small integers with Uns or Sgn abstract values.
This is a follow-up to commit 2932b53. It adds provenance tracking to the Uns and Sgn abstract values.
Diffstat (limited to 'backend/CSE.v')
| -rw-r--r-- | backend/CSE.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/CSE.v b/backend/CSE.v index e9006d4f..c0efa941 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -289,10 +289,10 @@ Definition kill_loads_after_store Definition store_normalized_range (chunk: memory_chunk) : aval := match chunk with - | Mint8signed => Sgn 8 - | Mint8unsigned => Uns 8 - | Mint16signed => Sgn 16 - | Mint16unsigned => Uns 16 + | Mint8signed => Sgn Ptop 8 + | Mint8unsigned => Uns Ptop 8 + | Mint16signed => Sgn Ptop 16 + | Mint16unsigned => Uns Ptop 16 | _ => Vtop end. |