Skip to content

if((int)(&a+2)) fails to warn about being unspecified

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


Id Project Category View Due Date Updated
ID0000077 Frama-C Plug-in > Eva public 2009-05-05 2014-02-12
Reporter pascal Assigned To pascal Resolution fixed
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C GIT, precise the release id Target Version - Fixed in Version Frama-C Beryllium-20090601-beta1

Description :

see summary. This is related to bug 76, which is fixed and partially fixes this problem too: at least the condition is correctly analyzed as being 0 or 1. But the policy is to emit an alarm (that is complicated to express, but that's another issue) and to consider the condition to be 1 modulo the verification of the alarm.

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