Wrong result in 30_Function_Pointer3_vs.c

[hernanponcedeleon]

The problem is due to the way we handle returns in the boogie code. Currently we assume there is only one return. The file mentioned in the title shoes that is not always the case.

[hernanponcedeleon]

For the time being we throw an exception when (unsupported) function pointers are used. Once we agree how to re-design/implement the whole parsing infrastructure, we need to come back to this issue and properly support function pointers.

[hernanponcedeleon]

We have problems (i.e., exception) to handle the function pointer, but at least we do not return a wrong result anymore. Closing.