GitLab

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