Skip to content

CIL's added return masks issues

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


Id Project Category View Due Date Updated
ID0000685 Frama-C Kernel public 2011-01-24 2012-09-19
Reporter virgile Assigned To virgile Resolution fixed
Priority normal Severity feature Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Carbon-20101202-beta2 Target Version - Fixed in Version Frama-C Oxygen-20120901

Description :

When an execution path in a function may fall through, CIL adds automatically a return statement. If the path is not unfeasible, this would mask an undefined behavior (6.9.1.14), as shown in the example below, where Frama-C would conclude that z is 0, while gcc reports 12:

int x;

int f(void) { x++; if (x<=10) return x-1; }

int main() { x = 11; int y = 42; int z = f(); return z; }

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