Frama-C-clang does not unfold typedef
ID0001805: This issue was created automatically from Mantis Issue 1805. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001805 | Frama-Clang | Kernel | public | 2014-06-12 | 2015-02-17 |
| Reporter | jens | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
When Frama-Clang analyses the following code example
struct A { int n; };
typedef struct A B;
/*@ requires \valid(b); assigns \nothing; ensures \result == b->n; / int foo(B b) { return b->n; }
then it complains
problem207.cpp:12:29: expecting a struct with field problem207.cpp:12:29: type is not a pointer type
Steps To Reproduce :
The source code of the example is available under acslplusplus/C++Examples/Problems/problem207.cpp It was analysed with the following command line:
frama-c.byte -cxx-clang-command="framaCIRGen" -wp problem207.cpp