| 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 |
|
Relationships 
Relationships