missing ";" after clause causes its tacit omission
ID0001976: This issue was created automatically from Mantis Issue 1976. Further discussion may take place here.
|ID0001976||Frama-Clang||Plug-in > clang||public||2014-11-20||2015-02-17|
|Product Version||-||Target Version||-||Fixed in Version||-|
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".