0000332: goto generated by Frama-C and not supported by Jessie

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000332

Frama-C

Kernel

public

2009-11-17 17:01

2010-04-13 15:33

Reporter

dpariente

Assigned To

virgile

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Frama-C Boron-20100401

Summary

0000332: goto generated by Frama-C and not supported by Jessie

Description

When slicing (or simply analyzing) a function like the following one:

void f(int*p,int e,int t,int f,int r)
{
  *p = ( (e || (t && f)) && (t || f) );
}

Frama-C translates it into:

/* Generated by Frama-C */
void f(int *p , int e , int t , int f_0 , int r )
{
  int tmp ;
  if (e) { goto _LOR; }
  else {
    if (t) {
      if (f_0) {
        _LOR: /* internal */ ;
        if (t) { tmp = 1; }
        else { if (f_0) { tmp = 1; } else { tmp = 0; } }
      }
      else { tmp = 0; }
    }
    else { tmp = 0; }
  }
  *p = tmp;
  return;
}

with a goto to a inner block.

But Jessie doesn't support this feature:
File "slicef.jc", line 42, characters 7-16: unsupported goto (backward
or to some inner block)

Category of this report is "kernel" as it is let up to Frama-C team to choose between an evolution of Jessie (in order to take this feature into account)
or a change in the way the Kernel (CIL) transforms boolean equations.

Tags

No tags attached.

Attached Files

Relationships

Notes
(0000619) virgile (developer) 2010-01-12 18:36	Jessie relies on ad'hoc normalization of C code, which it sets when -jessie is enabled. If it used on code pretty-printed by frama-c and re-parsed, the ad'hoc normalization phase is no longer possible (it must occur at the first parsing). A new option -jessie-adhoc-normalization will force such normalization even if the jessie analysis is not triggered (allowing for instance a slicing phase before it). Is this an acceptable work-around?

(0000620) dpariente (reporter) 2010-01-12 19:08	At a first glance, it seems OK. Thanks.

Issue History
Date Modified	Username	Field	Change
2009-11-17 17:01	dpariente	New Issue
2010-01-12 18:36	virgile	Note Added: 0000619
2010-01-12 18:36	virgile	Status	new => feedback
2010-01-12 19:08	dpariente	Note Added: 0000620
2010-01-13 17:01	virgile	Status	feedback => resolved
2010-01-13 17:01	virgile	Resolution	open => fixed
2010-01-13 17:01	virgile	Assigned To	=> virgile
2010-04-13 15:30	signoles	Status	resolved => new
2010-04-13 15:31	signoles	Status	new => closed
2010-04-13 15:33	signoles	Fixed in Version	=> Frama-C Boron