advanced adress arithmetic causes loss of source location
ID0001802: This issue was created automatically from Mantis Issue 1802. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0001802 | Frama-Clang | Plug-in > from | public | 2014-06-06 | 2015-02-20 |
Reporter | Jochen | Assigned To | virgile | Resolution | no change required |
Priority | normal | Severity | minor | Reproducibility | always |
Platform | - | OS | xubuntu-cfe13.10 | OS Version | - |
Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
output of "frama-c -deps from.c -slevel 10":
... [from] ====== DEPENDENCIES COMPUTED ====== These dependencies hold at termination for the executions that terminate: [from] Function main: publc2 FROM publc1 \result FROM \nothing [from] ====== END OF DEPENDENCIES ======
However, if "publc1" is located e.g. at address 0x30000, then "p" would point to 0x30004, that is, (possibly) to "secret1", which wasn't mentioned as source location by FromAnalysis.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information