0000877: RTE does not generate assertions for non initialized arguments

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000877

Frama-C

Plug-in > RTE

public

2011-07-06 10:10

2012-05-16 18:22

Reporter

yakobowski

Assigned To

pherrmann

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Frama-C Nitrogen-20111001

Summary

0000877: RTE does not generate assertions for non initialized arguments

Description

Calling the WP (or Jessie for that matter) on the following code results in all goals being proven. Yet, there is a RTE on the call to max, because a is not initialized. I tend to think that -rte-precond should add \initialized(a) and \initialized(b) to the local contract for the call to max, but there is perhaps another better way. Anyway, either RTE or the WP are faulty here. /*@ ensures \result == (a < b ? a : b); */ int max(int a, int b) { return (a < b ? a : b); } int main () { int a; int b = 2; return max (a, b); }

Tags

No tags attached.

Attached Files

Relationships

Notes
(0002010) yakobowski (manager) 2011-07-06 10:10	(Wp called with -wp-rte.)

(0002152) pherrmann (reporter) 2011-08-22 10:15	See svn 14739 for documentation update: RTE does not report usage of non initialized automatic variables. Would require a dataflow analysis to avoid an excessive number of generated annotations.

Issue History
Date Modified	Username	Field	Change
2011-07-06 10:10	yakobowski	New Issue
2011-07-06 10:10	yakobowski	Status	new => assigned
2011-07-06 10:10	yakobowski	Assigned To	=> pherrmann
2011-07-06 10:10	yakobowski	Note Added: 0002010
2011-08-22 10:15	pherrmann	Note Added: 0002152
2011-08-22 10:15	pherrmann	Status	assigned => resolved
2011-10-10 14:13	signoles	Fixed in Version	=> Frama-C Nitrogen-20111001
2011-10-10 14:14	signoles	Status	resolved => closed
2012-05-16 18:22	signoles	Resolution	open => fixed