assigns clause unchecked on arrays
ID0000443: This issue was created automatically from Mantis Issue 443. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000443 | Frama-C | Plug-in > jessie | public | 2010-04-06 | 2010-04-19 |
| Reporter | Jochen | Assigned To | cmarche | Resolution | fixed |
| Priority | urgent | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Beryllium-20090902 | Target Version | Frama-C Boron-20100401 | Fixed in Version | Frama-C Boron-20100401 |
Description :
While 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".