assert-clause recommended by tool doesn't make warning vanish
ID0000863: This issue was created automatically from Mantis Issue 863. Further discussion may take place here.
|ID0000863||Frama-C||Plug-in > Eva||public||2011-06-10||2011-06-10|
|Reporter||Jochen||Assigned To||pascal||Resolution||no change required|
|Product Version||Frama-C Carbon-20110201||Target Version||-||Fixed in Version||-|
When running "frama-c -val ftest.c" on the attached program, I get the messages: ftest.c:4:[value] Assertion got status unknown. ftest.c:5:[kernel] warning: out of bounds read. assert \valid(argv+0);
However, the assertion recommended in the above warning is already in the code (in line 4); so I'd expect the warning to have vanished.