0002123: validity of obligation from statement contract depends on whether the statement is enclosed in block {}

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

Notes
(0005952) correnson (manager) 2015-06-29 16:54	This is very surprising, It seems that labels in function calls are not correctly treated.

(0005953) correnson (manager) 2015-06-29 16:55	I must investigate the problem.

Issue History
Date Modified	Username	Field	Change
2015-06-01 12:42	Jochen	New Issue
2015-06-01 12:42	Jochen	Status	new => assigned
2015-06-01 12:42	Jochen	Assigned To	=> correnson
2015-06-01 12:42	Jochen	File Added: 480.c
2015-06-01 12:42	Jochen	File Added: in_block_foo_stmt_post_Alt-Ergo.mlw
2015-06-01 12:42	Jochen	File Added: not_in_block_foo_stmt_post_Alt-Ergo.mlw
2015-06-29 16:54	correnson	Note Added: 0005952
2015-06-29 16:55	correnson	Note Added: 0005953
2015-06-29 16:55	correnson	Status	assigned => acknowledged