View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
ID | Project | Category | View Status | Date Submitted | Last Update |
0002123 | Frama-C | Plug-in > wp | public | 2015-06-01 12:42 | 2015-06-29 16:55 |
|
Reporter | Jochen | |
Assigned To | correnson | |
Priority | normal | Severity | minor | Reproducibility | always |
Status | acknowledged | Resolution | open | |
Platform | Sodium-20150201 | OS | | OS Version | xubuntu14.04 |
Product Version | Frama-C Sodium | |
Target Version | | Fixed in Version | | |
|
Summary | 0002123: validity of obligation from statement contract depends on whether the statement is enclosed in block {} |
Description | Running "frama-c -wp 480.c" on the attached program produces one unproven Alt-Ergo obligation (see file "in_block_foo_stmt_post_Alt-Ergo.mlw").
If the block parentheses in line 16 and 23 are removed, the corresponding obligation (file "not_in_block_foo_stmt_post_Alt-Ergo.mlw") is proven.
The differences between both obligations files are:
772c772
< forall t_2,t_1 : (addr,int) farray.
---
> forall t_1 : (addr,int) farray.
780c780
< (1 = L_deref(t_2, a))
---
> (1 = L_deref(t_1, a))
So, enclosing the statement in a block apparently creates an unrelated memory state.
|
Tags | No tags attached. |
|
Attached Files | 480.c [^] (311 bytes) 2015-06-01 12:42 [Show Content] [Hide Content]
/*@
axiomatic ax1 {
logic integer deref{L}(int* a) reads *a;
axiom ax2{L}: \forall int* a; deref(a) == *a;
}
*/
/*@
requires \valid(a);
requires *a == 1;
assigns \nothing;
*/
void foo(int* a) {
int x = 5;
{
/*@
requires *a == 1;
assigns \nothing;
ensures deref(a) == 1;
*/
;
}
}
in_block_foo_stmt_post_Alt-Ergo.mlw [^] (31,027 bytes) 2015-06-01 12:42
not_in_block_foo_stmt_post_Alt-Ergo.mlw [^] (31,023 bytes) 2015-06-01 12:42 |
|