unbound logic variable INT_MAX ,why?
ID0000545: This issue was created automatically from Mantis Issue 545. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000545 | Frama-C | Kernel > ACSL implementation | public | 2010-07-19 | 2010-07-19 |
| Reporter | luoting | Assigned To | virgile | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
When I run ' frama-c -jessie a.c', it goes as follows: [kernel] preprocessing with "gcc -C -E -I. -dD a.c" a.c:22:[kernel] user error: Error during annotations analysis: unbound logic variable INT_MAX My frama-c version is Beryllium-20090902 and why is 2.23.
Additional Information :
#include <limits.h> However ,when I try another example b.c ' int sqsum(int* p, int n) { int S=0, tmp; for(int i = 0; i < n; i++) { //@ assert p[i] * p[i] <= INT_MAX; tmp = p[i] * p[i]; //@ assert tmp >= 0; //@ assert S + tmp <= INT_MAX; S += tmp; } return S; } ' Gwhy can generate VC . [kernel] preprocessing with "gcc -C -E -I. -dD b.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir b.jessie [jessie] File b.jessie/b.jc written. [jessie] File b.jessie/b.cloc written. [jessie] Calling Jessie tool in subdir b.jessie Generating Why function sqsum [jessie] Calling VCs generator. gwhy-bin [...] why/b.why Computation of VCs... Computation of VCs done. Reading GWhy configuration... Loading .gwhyrc config file GWhy configuration loaded... Creating GWhy Tree view... GWhy Tree view created... Creating GWhy views... Saving .gwhyrc config file GWhy views created.