Code containing consts should be verifiable
ID0000485: This issue was created automatically from Mantis Issue 485. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000485 | Frama-C | Plug-in > jessie | public | 2010-05-18 | 2010-05-18 |
| Reporter | boris | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Beryllium-20090902 | Target Version | - | Fixed in Version | - |
Description :
Jessie should be able to verify code that contains global C-constants as declared with the keyword const.
I consider using consts instead of macros good programming practice.
Additional Information :
// Doesn't verify:
const int size=4;
/*@ requires \valid(msg+(0..size)); / int setFoo(char msg) { msg[size] = '\0'; return 0; }