0002180: Crash on loop with global assigns and per-behavior assigns

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002180

Frama-C

Plug-in > wp

public

2015-10-19 21:31

2017-12-17 20:53

Reporter

yakobowski

Assigned To

correnson

Priority

normal

Severity

crash

Reproducibility

always

Status

assigned

Resolution

open

Platform

OS Version

Product Version

Target Version

Fixed in Version

Summary

0002180: Crash on loop with global assigns and per-behavior assigns

Description

frama-c -wp crashes on the following program

/*@ behavior foo:
       */
void main(void)
{
  int i;
  int t[10];
  i = 0;
  /*@ loop assigns t[0 .. i];
      for foo: loop assigns t[0 .. i]; */
  while (i < 10) {
    t[i] = 0;
    i ++;
  }
  return;
}

Tags

No tags attached.

Attached Files

Relationships

Notes
There are no notes attached to this issue.

Issue History
Date Modified	Username	Field	Change
2015-10-19 21:31	yakobowski	New Issue
2015-10-19 21:31	yakobowski	Status	new => assigned
2015-10-19 21:31	yakobowski	Assigned To	=> correnson