ID0001976: **This issue was created automatically from Mantis Issue 1976. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001976 | Frama-Clang | Plug-in > clang | public | 2014-11-20 | 2015-02-17 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open | | **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 : The goal "typed_main_assert" generated from the file "141.cpp" can't be proven; the corresponding .mlw file contains the goal formula "goal main_assert: forall i : int. is_sint32(i) -> (111 = i)"; that is, the "ensures" clause from line 2 isn't used there. If the missing ";" at the end of line 2 is appended, the generated goal reads "goal main_assert: forall i : int. (222 = (2 * i)) -> is_sint32(i) -> (111 = i)", and is proven by Alt-Ergo. No warning or error message about the missing ";" is issued. When the file is renamed to "141.c", frama-c prints an error message "141.c:2:[kernel] user error: expecting ';' before end of annotation". ## Attachments - [141.cpp](/uploads/a78879845eac9a5610cf9c89525d755d/141.cpp)