0000041: Inability to prove assigns clauses on simple array code

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000041

Frama-C

Plug-in > jessie

public

2009-04-07 15:36

2009-06-23 18:03

Reporter

virgile

Assigned To

cmarche

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Lithium-20081201

Target Version

Frama-C Beryllium-20090601-beta1

Fixed in Version

Frama-C Beryllium-20090601-beta1

Summary

0000041: Inability to prove assigns clauses on simple array code

Description

[bug 7560 from old bts, reported by David Mentré]
Hello,

With this code:
----
#include <string.h>

#define MAX 12

int a[MAX];
char *c[MAX];

/*@ assigns a[..];
*/
void assign_int(void)
{
  int i;

  //@ loop invariant 0 <= i && i <= MAX;
  for (i = 0; i < MAX; i++) {
    a[i] = 0x45;
  }
}

/*@ assigns c[..];
*/
void assign_char(void)
{
  int i;

  //@ loop invariant 0 <= i && i <= MAX;
  for (i = 0; i < MAX; i++) {
    c[i] = strndup("something", MAX);
  }
}

/*@ assigns a[..];
    assigns c[..];
*/
void main(void)
{
  assign_int();
  assign_char();
}
------

On this code, I cannot prove properties "assigns a[..];" for
assign_int() and "assigns c[..];" for assign_char(). However the
assignation seems obvious to me.

I have tried "assigns a[0..11];" without success.

Is assigns broken?

Boris had a similar issue:
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-April/000487.html [^]

Yours,
d.

Tags

No tags attached.

Attached Files

Relationships

Notes
There are no notes attached to this issue.

Issue History
Date Modified	Username	Field	Change
2009-04-07 15:36	virgile	New Issue
2009-04-07 15:40	signoles	Status	new => acknowledged
2009-04-30 16:48	monate	Status	acknowledged => assigned
2009-04-30 16:48	monate	Assigned To	=> cmarche
2009-06-04 15:16	cmarche	Target Version	=> Frama-C Beryllium
2009-06-18 13:41	cmarche	Resolution	open => fixed
2009-06-18 13:42	cmarche	Status	assigned => resolved
2009-06-23 18:02	signoles	Status	resolved => closed
2009-06-23 18:03	signoles	Fixed in Version	=> Frama-C Beryllium beta-1