ID0002042: **This issue was created automatically from Mantis Issue 2042. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002042 | Frama-Clang | Plug-in > clang | public | 2015-01-05 | 2015-02-15 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 | | **Product Version** | - | **Target Version** | - | **Fixed in Version** | - | ### Description : Using "frama-c -wp 424.cpp" the attached program can be verified, although e.g. foo<int>(0) yields 2 whereas its contract says it should yield 4. Apparently, Frama-C thinks the contract belongs to the plain function bar(). That would also be an explanation for issue #2034. Moving the contract from line 4 down to line 6, or to line 8, keeps that behavior. After moving it up to line 1 (i.e. before the generic template), no obligation at all is generated (which is ok since foo<>() isn't called anywhere). ## Attachments - [424.cpp](/uploads/27785eb453be4b53b4f7843126234b75/424.cpp) - [424a.cpp](/uploads/8bcfdd48f28c3257a7b0dbdfd882ce36/424a.cpp)