0000384: Labels in loops are not unrolled - Frama-C Bug Tracking System

Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0000384

Frama-C

Kernel

public

2010-01-29 17:13

2012-09-19 17:16

Reporter

gmelquio

Assigned To

virgile

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Frama-C Oxygen-20120901

Summary

0000384: Labels in loops are not unrolled

Description

For the following testcase with revision 7516, the Jessie output doesn't contain copies of label L in the unrolled parts of the loop, causing the unrolled assertions to be dangling.

int main() {
  int i, j;
  j = 0;
  /*@ loop pragma UNROLL 4; */
  for (i = 0; i <= 2; ++i) {
    L:
    j = j + 1;
    //@assert j == \at(j,L) + 1;
  }
}

Tags

No tags attached.

Relationships

Notes
(0000655) virgile (developer) 2010-01-29 18:07	Distinct copies of the label are made in the code, but this is not reflected in the ACSL comment...

(0002831) yakobowski (manager) 2012-04-05 01:00	This has been corrected recently by either Virgile or Patrick. Loop unrolling should be much more robust.

Issue History
Date Modified	Username	Field	Change
2010-01-29 17:13	gmelquio	New Issue
2010-01-29 18:06	virgile	Status	new => assigned
2010-01-29 18:06	virgile	Assigned To	=> virgile
2010-01-29 18:07	virgile	Note Added: 0000655
2010-01-29 18:07	virgile	Status	assigned => acknowledged
2012-04-05 01:00	yakobowski	Note Added: 0002831
2012-04-05 01:00	yakobowski	Status	acknowledged => resolved
2012-04-05 01:00	yakobowski	Resolution	open => fixed
2012-09-19 17:15	signoles	Fixed in Version	=> Frama-C Oxygen-20120901
2012-09-19 17:16	signoles	Status	resolved => closed

Copyright © 2000 - 2019 MantisBT Team