Logic with read clauses can have their values invalidated by writes to separated memory locations
ID0002244: This issue was created automatically from Mantis Issue 2244. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002244 | Frama-C | Plug-in > wp | public | 2016-08-08 | 2016-08-08 |
| Reporter | jrobbins | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Aluminium | Target Version | - | Fixed in Version | - |
Description :
In some cases, axiomatic logic using reads clauses can be true for a certain memory location, and then become unknown once an unrelated memory location is assigned to. You can even prove the memory locations as separate, but it does not fix the issue.
Additional Information :
This bug is present on both Frama-C versions Sodium and Aluminum.
Steps To Reproduce :
== File bug.c: /*@ axiomatic Axiomatic { logic boolean property_of_buffer(char *buffer) reads *buffer; } */
/*@ assigns *buffer; ensures property_of_buffer(buffer); */ void foo(char *buffer);
/*@ requires property_of_buffer(buffer); assigns *buffer; ensures property_of_buffer(buffer); */ int bar(char *buffer);
char buf1[1]; char buf2[1];
void main() { foo(buf1); bar(buf1);
foo(buf2);
bar(buf1);} == Command to run: frama-c -wp bug.c == Output: [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing bug.c (with preprocessing) [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 2 goals scheduled [wp] [Qed] Goal typed_main_call_bar_pre : Valid [wp] [alt-ergo] Goal typed_main_call_bar_pre_2 : Unknown (562ms) [wp] Proved goals: 1 / 2 Qed: 1 alt-ergo: 0 (unknown: 1) == Expected behavior: For typed_main_call_bar_pre_2 to prove valid.