0000673: untypable ACSL in a sliced program containing \result

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000673

Frama-C

Plug-in > slicing

public

2011-01-17 16:33

2014-02-12 16:55

Reporter

signoles

Assigned To

patrick

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Carbon-20101202-beta2

Target Version

Fixed in Version

Frama-C Carbon-20110201

Summary

0000673: untypable ACSL in a sliced program containing \result

Description

If a function contract contains \result, then the sliced function keeps it even if it now returns void.

Steps To Reproduce

===== bug.c ===== void f(void) { return; } /*@ ensures \result == 0; */ int main(void) { f(); return 0; } ================== $ frama-c bug.c -slice-calls f -then-on "Slicing export" -print -ocode sliced_bug.c $ more sliced_bug.c /* Generated by Frama-C */ void f_slice_1(void) { return; } /*@ ensures (\result ? 0); */ void main(void) { f_slice_1(); return; } $ frama-c sliced_bug.c [kernel] preprocessing with "gcc -C -E -I. sliced_bug.c" sliced_bug.c:7:[kernel] user error: \result meaningless in annotation. [kernel] user error: skipping file "sliced_bug.c" that has errors. [kernel] Frama-C aborted because of invalid user input.

Tags

No tags attached.

Attached Files

Relationships

Notes
(0001391) Anne (reporter) 2011-01-17 16:59	Mmm... it seems that it comes from a bug in Pdg function [find_fun_postcond_nodes] in [annot.ml]. I must look deeper to find what it is...

(0001396) Anne (reporter) 2011-01-18 09:52	The function used to know which zones (data) are needed to interpret a predicate is [!Db.Properties.Interp.To_zone.from_pred] with [!Db.Properties.Interp.To_zone.mk_ctx_func_contrat] request. The problem is that the \result is not really a 'zone'. I guess I need another function to test if \result is used in a postcondition because it would be to difficult to change [from_pred] signature since it is used for several different purposes. What do you think, Patrick ?

(0001399) Anne (reporter) 2011-01-18 16:43	@Patrick: I have added a comment to [find_fun_postcond_nodes] in [annot.ml] to give a hint of how to use the previous result.

Issue History
Date Modified	Username	Field	Change
2011-01-17 16:33	signoles	New Issue
2011-01-17 16:33	signoles	Status	new => assigned
2011-01-17 16:33	signoles	Assigned To	=> Anne
2011-01-17 16:35	signoles	Summary	unparsable ACSL in a sliced program containing \result => untypable ACSL in a sliced program containing \result
2011-01-17 16:59	Anne	Note Added: 0001391
2011-01-17 16:59	Anne	Status	assigned => acknowledged
2011-01-18 09:52	Anne	Note Added: 0001396
2011-01-18 09:52	Anne	Status	acknowledged => assigned
2011-01-18 09:52	Anne	Assigned To	Anne => patrick
2011-01-18 09:53	Anne	Note View State: 1391: public
2011-01-18 16:43	Anne	Note Added: 0001399
2011-01-19 16:52	svn	Checkin
2011-01-19 16:52	svn	Status	assigned => resolved
2011-01-19 16:52	svn	Resolution	open => fixed
2011-02-09 14:36	signoles	Status	resolved => closed
2011-02-09 14:37	signoles	Fixed in Version	=> Frama-C Carbon-20110201