0002312: false postcondition shouldn't be verified in default memory-model setting

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002312

Frama-C

Plug-in > wp

public

2017-06-15 13:39

2017-06-15 15:14

Reporter

Jochen

Assigned To

correnson

Priority

normal

Severity

tweak

Reproducibility

always

Status

assigned

Resolution

open

Platform

Phosphorus-20170501-beta1

xubuntu

OS Version

Product Version

Frama-C 15-Phosphorus

Target Version

Fixed in Version

Summary

0002312: false postcondition shouldn't be verified in default memory-model setting

Description

Running "frama-c -wp -wp-rte memmodel_default.c" verifies all 11 proof obligations, while the assert clase in line 21 is obviously violated. The reason for Frama-C's behavior is that it assumes the "Hoare Variables mixed with Pointers" memory model as a default (in accordance with WP manual sect.3.4, p.45) without checking its preconditions, viz. the absence of any address-taking of a variable.

A novice user who doesn't yet know about the subtleties of memory models will assume after the above Frama-c run that the program is ok, as is has been formally verified. This may build up unjustified trust in the program, and discredit Frama-C (or even the whole field of formal methods) once the bug is detected at runtime, possibly causing severe damage.

I suggest to either
1. check the applicability of the "Hoare Variables mixed with Pointers" model (this should be easily achievable, if only the source code needs to be scanned for a unary "&"), or
2. use another, less restrictive, model as default.

Tags

No tags attached.

Attached Files

memmodel_default.c [^] (273 bytes) 2017-06-15 13:39 [Show Content] [Hide Content]

static int g;

/*@
	requires \valid(x);
	requires 0 <= *x <= 10;
	requires 0 <= g  <= 10;
	ensures *x == \old(*x) + 1;
	ensures g  == \old(g ) + 1;
*/
void foo(int *x) {
	*x += 1;
	g  += 1;
}


void bar(void) {
	g = 3;
	//@ assert g == 3;
	foo(&g);
	//@ assert g == 4;
}

Relationships

Notes
(0006410) Jochen (reporter) 2017-06-15 15:10	Running "frama-c -wp -wp-rte memmodel_default.c -wp-model ref" on the above program verifies all obligations, too. This contradicts the WP manual Sect.3.5 "Hoare Variables for Reference Parameters", p.46, which says "necessary separation conditions are generated on-the-fly". Apparently, no condition "requires \separated(&g,x);" is genarated for foo. If that condition is added manually, it can't be verified (as expected).

Issue History
Date Modified	Username	Field	Change
2017-06-15 13:39	Jochen	New Issue
2017-06-15 13:39	Jochen	Status	new => assigned
2017-06-15 13:39	Jochen	Assigned To	=> correnson
2017-06-15 13:39	Jochen	File Added: memmodel_default.c
2017-06-15 15:10	Jochen	Note Added: 0006410