value analysis assumes dynamic_cast between unrelated classes to succeed, rather than to yield NULL
ID0002076: This issue was created automatically from Mantis Issue 2076. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002076 | Frama-Clang | Plug-in > clang | public | 2015-02-09 | 2015-04-01 |
| Reporter | Jochen | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | Neon-20140301+dev-STANCE-Jan2015 | OS | - | OS Version | xubuntu-cfe13.10 |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -val 461.cpp" on the attached program yields the output (excerpt):
461.cpp:10:[value] Assertion got status valid.
However, running "clang++ 461.cpp && ./a.out" reveals that the assertion in line 12 (identical to that in line 11) is in fact invalid:
a.out: 461.cpp:11: int main(): Assertion `bp!=0' failed.
Compiling "g++ 461.cpp" even yields a compile-time warning:
461.cpp: In function ‘int main()’: 461.cpp:9:37: warning: dynamic_cast of ‘A aaa’ to ‘struct B*’ can never succeed [enabled by default] B* const bp = dynamic_cast<B*>(&aaa); ^