missing ";" after clause causes its tacit omission
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".