Warning for Axiom: From wp: Overloaded operator User defined axiom
ID0000896: This issue was created automatically from Mantis Issue 896. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000896 | Frama-C | Plug-in > wp | public | 2011-07-28 | 2014-02-12 |
| Reporter | patrick | Assigned To | correnson | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
Since there is no overloading is the source, the warning message has no sense!
Additional Information :
cat file.c extern int tab[], x; //@ axiomatic A { axiom ax: 10 < \block_length(tab); } //@ assigns x; extern void h(void); //@ requires r2: x==0; assigns x; void g() { h(); } //@ requires r1: x==0; void f(void) { g(); }
frama-c -wp ... file.c:8:[wp] warning: Warning for Axiom ax: From wp: Overloaded operator User defined axiom ax{L} and User defined axiom ax {L} not yet implemented Effect: Ignored user-defined axiom 'ax'