Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 02:52 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000443Frama-CPlug-in > jessiepublic2010-04-19 16:14
ReporterJochen 
Assigned Tocmarche 
PriorityurgentSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Beryllium-20090902 
Target VersionFrama-C Boron-20100401Fixed in VersionFrama-C Boron-20100401 
Summary0000443: assigns clause unchecked on arrays
DescriptionWhile a write-access to a simple variable (int a) is recognized to violate an assigns-clause, a similar access to an array variable (int a[1]) is not.

No proof obligation is generated in the latter case.

See attached file; uncomment / comment-out the #define to demonstrate the different behaviors.

I tried jessie only without the option "-jessie-no-regions".
TagsNo tags attached.
Attached Files
  • c file icon ftest.c (209 bytes) 2010-04-06 16:55 -
    // uncomment to make proof-obligation for line 10 vanish:
    //#define array
    
    #ifdef array
    int a[1];
    #else
    int a;
    #endif
    
    //@ assigns \nothing;
    void f(void) {
    #ifdef array
        a[0] = 3;
    #else
        a = 3;
    #endif
    }
    
    c file icon ftest.c (209 bytes) 2010-04-06 16:55 +

-Relationships
+Relationships

-Notes

~0000756

cmarche (developer)

Fixed in current SVN of Why.

The fix exposes another bug when adress of a local variable is taken (see ref.c dillon1.c, dillon3.c), where an incorrect Why program is now generated.

The fix is preferable than nothing, because the original bug was a major one.


~0000774

signoles (manager)

Fix in Why 2.24 (require Frama-C Boron-20100401).
+Notes

-Issue History
Date Modified Username Field Change
2010-04-06 16:55 Jochen New Issue
2010-04-06 16:55 Jochen Status new => assigned
2010-04-06 16:55 Jochen Assigned To => cmarche
2010-04-06 16:55 Jochen File Added: ftest.c
2010-04-08 13:01 cmarche Priority normal => urgent
2010-04-08 14:28 cmarche Assigned To cmarche =>
2010-04-08 14:30 cmarche Assigned To => cmarche
2010-04-08 14:30 cmarche Target Version => Frama-C Boron
2010-04-08 16:53 cmarche Note Added: 0000756
2010-04-08 16:53 cmarche Status assigned => resolved
2010-04-08 16:53 cmarche Resolution open => fixed
2010-04-19 16:13 signoles Status resolved => closed
2010-04-19 16:13 signoles Fixed in Version => Frama-C Boron
2010-04-19 16:14 signoles Note Added: 0000774
+Issue History