Skip to content

Incorrect results with low slevel

ID0000844: This issue was created automatically from Mantis Issue 844. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000844 Frama-C Plug-in > Eva public 2011-05-28 2011-10-10
Reporter yakobowski Assigned To pascal Resolution fixed
Priority normal Severity major Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Carbon-20110201 Target Version - Fixed in Version Frama-C Nitrogen-20111001

Description :

The following program is correct and always terminates. However, with no slevel, the value analysis incorrectly states that main and memset do not terminate.

(Analyzed with -value -slevel 0)

void* memset (void* dest, int val, unsigned int len) { unsigned char ptr = (unsigned char)dest; while (len-- > 0) { *ptr++ = val; } return dest; }

extern int k;

void main () { int v; int x = k ? 2 : 3; memset(&v,42,x); }

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information