| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0002330 | Frama-C | Plug-in > wp | public | 2017-10-26 12:55 | 2020-02-17 18:08 |
|
| Reporter | Jochen | |
| Assigned To | correnson | |
| Priority | normal | Severity | minor | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | Phosphorus-20170501 | OS | | OS Version | xubuntu 17.04 |
| Product Version | | |
| Target Version | | Fixed in Version | Frama-C 20-Calcium | |
|
| Summary | 0002330: known, but inferrable, yet not inferred, property not given as precodition to provers |
| Description | Running "frama-c -wp foo.c -wp-out wp-out -wp-prop=D" on the attached program fails to prove the property D, although it follows immediately from A and C.
A look at the generated file "foo_assert_D_Alt-Ergo.mlw" reveals that the condition "y<=15" from C is not given to Alt-Ergo, while "0<=y" is.
If the former is inserted into the mlw file, Alt-Ergo proves the goal without problems.
Probably, "y<=15" is considered a trivial consequence of "y==(x&0xf)" by Qed; however, it shouldn't, since (e.g.) Alt-Ergo is unable to to infer this: goal C cannot be proven by Alt-Ergo. |
| Steps To Reproduce | Name translation c -> mlw for convenience:
x -> i
y -> x
z -> x_1
|
| Tags | No tags attached. |
|
| Attached Files |  foo.c [^] (246 bytes) 2017-10-26 12:55 [Show Content] [Hide Content]
extern int a[16];
/*@ requires A: \forall integer i; 0 <= i <= 15 ==> 0 <= a[i] <= 9;
requires B: 0 <= x <= 255;
*/
void foo(int x) {
int const y = (x & 0xf);
//@ assert C: 0 <= y <= 15;
int const z = a[y];
//@ assert D: 0 <= z <= 9;
}
|
|
Relationships 
Relationships