Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000332Frama-CKernelpublic2009-11-17 17:012010-04-13 15:33
Reporterdpariente 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000332: goto generated by Frama-C and not supported by Jessie
DescriptionWhen 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.
TagsNo 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker