0000861: Incorrect loop unrolling in presence of switch - Frama-C Bug Tracking System

Frama-C Bug Tracking System

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

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0000861

Frama-C

Kernel

public

2011-06-09 21:18

2014-02-12 16:59

Reporter

yakobowski

Assigned To

yakobowski

Priority

high

Severity

crash

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Frama-C Carbon-20110201

Target Version

Fixed in Version

Frama-C Nitrogen-20111001

Summary

0000861: Incorrect loop unrolling in presence of switch

Description

Syntactic loop unrolling of loops containing while is completely wrong.
Can be checked with -print or -check on the code below.

void main () {
  /*@ loop pragma UNROLL_LOOP 4; */
  for (int i=0;i<4;i++) {
    switch (i) {
    case 1: break;
    case 2: break;
    case 3: break;
    case 4: break;
    default:
    }
  }
}

Tags

No tags attached.

Relationships

Notes
(0001965) yakobowski (manager) 2011-06-09 23:52	Virgile, if you have some time, please check the fix.

(0004774) yakobowski (manager) 2014-02-12 16:59	Fix committed to stable/neon branch.

Issue History
Date Modified	Username	Field	Change
2011-06-09 21:18	yakobowski	New Issue
2011-06-09 21:20	yakobowski	Status	new => assigned
2011-06-09 21:20	yakobowski	Assigned To	=> virgile
2011-06-09 23:52	yakobowski	Note Added: 0001965
2011-06-09 23:52	svn	Checkin
2011-06-09 23:52	svn	Status	assigned => resolved
2011-06-09 23:52	svn	Resolution	open => fixed
2011-10-10 14:13	signoles	Fixed in Version	=> Frama-C Nitrogen-20111001
2011-10-10 14:14	signoles	Status	resolved => closed
2014-02-12 16:59	yakobowski	Note Added: 0004774
2014-02-12 16:59	yakobowski	Assigned To	virgile => yakobowski
2014-02-12 16:59	yakobowski	Status	closed => resolved

Copyright © 2000 - 2017 MantisBT Team