0001135: unrolling loop statements with labels into there annotations are not handled correctly (in conjunction with -ulevel)

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

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001135

Frama-C

Kernel

public

2012-03-27 10:52

2014-02-12 16:59

Reporter

patrick

Assigned To

patrick

Priority

normal

Severity

major

Reproducibility

have not tried

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Frama-C Oxygen-20120901

Summary

0001135: unrolling loop statements with labels into there annotations are not handled correctly (in conjunction with -ulevel)

Description

Fresh labels and correct gotos are introduced when unrolling loop statements,
but labels into code annotations are not handled correctly.

Into the given example, the assertion is not unrolled correctly.

Additional Information

> cat file.c
int X ;
void main (int c) {
  for (int i = 0 ; i < 10 ;) {
    if (c) goto there ;
    X++;
  there: i++;
    //@ assert c==0 ==> \at(X,there)==i+1;
  }
}

> frama-c file.c -ulevel 1 -print
int X;
void main(int c)
{
  int i;
  i = 0;
  if (! (i < 10)) { goto unrolling_2_loop; }
  if (c) { goto there_unrolling_4_loop; }
  X ++;
  there_unrolling_4_loop: /* internal */ i ++;
  /*@ assert c ? 0 ? \at(X,there) ? i+1; */ ;
  unrolling_3_loop: /* internal */ ;
  while (i < 10) {
    if (c) { goto there; }
    X ++;
    there: i ++;
    /*@ assert c ? 0 ? \at(X,there) ? i+1; */ ;
  }
  unrolling_2_loop: /* internal */ ;
  return;
}

Tags

No tags attached.

Attached Files

Relationships

Notes
(0004710) patrick (developer) 2014-02-12 16:59	Fix committed to stable/neon branch.

Issue History
Date Modified	Username	Field	Change
2012-03-27 10:52	patrick	New Issue
2012-03-27 10:55	patrick	Status	new => assigned
2012-03-27 10:55	patrick	Assigned To	=> patrick
2012-03-27 11:02	signoles	Assigned To	patrick => virgile
2012-03-28 08:12	svn	Checkin
2012-03-28 08:12	svn	Status	assigned => resolved
2012-03-28 08:12	svn	Resolution	open => fixed
2012-04-02 13:59	svn	Checkin
2012-09-19 17:15	signoles	Fixed in Version	=> Frama-C Oxygen-20120901
2012-09-19 17:16	signoles	Status	resolved => closed
2014-02-12 16:59	patrick	Note Added: 0004710
2014-02-12 16:59	patrick	Assigned To	virgile => patrick
2014-02-12 16:59	patrick	Status	closed => resolved