ID0002007: **This issue was created automatically from Mantis Issue 2007. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002007 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-02-16 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open | | **Priority** | normal | **Severity** | feature | **Reproducibility** | always | | **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 | | **Product Version** | - | **Target Version** | - | **Fixed in Version** | - | ### Description : Output of "frama-c -wp 185.cpp" in its current version: 185.cpp:4:24: comparison of incompatible types Now output intermediate result 185.cpp:4:[kernel] user error: comparison of incompatible types: struct _Z1X and ℤ in annotation. [kernel] user error: skipping file "185.cpp" that has errors. [kernel] Frama-C aborted: invalid user input. Output of the same command after deleting "< 9" (or, alternatively, deleting "0 <") in line 4: 185.cpp:4:20: comparison of incompatible types 185.cpp:4:20: expecting a term or predicate 185.cpp:4:20: expecting a predicate Now output intermediate result [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 0 goal scheduled [wp] Proved goals: 0 / 0 While both behaviors of Frama-C are ok, their difference (in particular not running / running the Wp plugin) could indicate a bug. ## Attachments - [185.cpp](/uploads/b1c887234898b1febb2313938115a12a/185.cpp)