Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002131Frama-CKernelpublic2015-06-04 21:042016-01-26 13:38
ReporterIan 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSUbuntuOS Version
Product VersionFrama-C Sodium 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0002131: Error with casted ternary statements
DescriptionThe following is a simplified version from an situation where macros created a statement (which had side effects, unlike this example).

  1 void main() {
  2 int p=0, i=0, j=0;
  3 // (char)( p ? i : j ); // [kernel] user error: cannot cast from void to char
  4 ( p ? i : j );
  5 }

When line three is uncommented, frama-c fails with the error noted. Inspecting the normalized version reveals a potential problem (line 3 is commented out).

> frama-c void_cast.c -then -print
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing void_cast.c (with preprocessing)
/* Generated by Frama-C */
void main(void)
{
  int p;
  int i;
  int j;
  p = 0;
  i = 0;
  j = 0;
  if (p) {
    if (i) ;
  }
  else
    if (j) ;
  return;
}

As seen above, line 4 is normalized to
  if (p) {
    if (i) ;
  }
  else
    if (j) ;

Which has two potential problems. First, it is unclear why ‘i' and ‘j’ are wrapped in conditionals. Second, this structure may result in the ‘if’ statement being casted, instead of ‘i' or ‘j’, ultimately producing the observed error.

Running just the gcc preprocessor on the initial source file does not cause these transformations.

> gcc -E void_cast.c
# 1 "void_cast.c"
# 1 "<built-in>"
# 1 "<command-line>"
# 1 "void_cast.c"
void main() {
    int p=0, i=0, j=0;
    (char)( p ? i : j );
    ( p ? i : j );
}

Interestingly, adding an assignment produces a reasonable transformation. The program:

void main() {
    int p=0, i=0, j=0;
    char c = (char)( p ? i : j );
}

Is normalized to:

void main(void)
{
  int p;
  int i;
  int j;
  char c;
  int tmp;
  p = 0;
  i = 0;
  j = 0;
  if (p) tmp = i; else tmp = j;
  c = (char)tmp;
  return;
}
Steps To ReproduceCreate file void_cast.c:
void main() {
    int p=0, i=0, j=0;
    (char)( p ? i : j );
}

Run frama-c:
> frama-c void_cast.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing void_cast.c (with preprocessing)
void_cast.c:3:[kernel] user error: cannot cast from void to char
[kernel] user error: stopping on file "void_cast.c" that has errors. Add '-kernel-msg-key pp'
                     for preprocessing command.
[kernel] Frama-C aborted: invalid user input.

But expected frama-c to succeed since the program is accepted by gcc.
TagsNo tags attached.
Attached Files

- Relationships
related to 0002117closedyakobowski frama-c gets confused by comma operator inside ternary operator: cannot cast from void to char 

-  Notes
(0005933)
yakobowski (manager)
2015-06-08 13:12

This problem has been solved at the same time as bug 0002117. The fix will be part of the next open source release of Frama-C. Can you also upload the original code (with the side effects), so that we may check that our fix is good?

Regarding the additional 'ifs': Frama-C preserves side effects that may cause undefined behavior (such as '1/x;') using a conditional with no 'then' or 'else' branch. This is why the two 'if(i)' and 'if(j)' are added. We use this construct because no other kind of statement is available to represent 'i;' or '1/x;'.
(0005934)
Ian (reporter)
2015-06-08 18:56

The original code comes from the NASA Core Flight Executive framework 6.4.0, available at http://sourceforge.net/projects/coreflightexec/ [^]

The file cfe_fs_decompress.c uses the macro NEXTBYTE() as a statement which expands to

(uint8)( gz_inptr<gz_insize ? gz_inbuf[gz_inptr++] : FS_gz_fill_inbuf() );
(0005935)
yakobowski (manager)
2015-06-08 21:21

I can confirm that the code the next version of Frama-C generates will be correct for this code pattern. An intermediate variable is introduce to represent gz_inbuf[gz_inptr++] or FS_gz_fill_inbuf() (typed as their smallest supertype). Then this variable is cast to uint8.

- Issue History
Date Modified Username Field Change
2015-06-04 21:04 Ian New Issue
2015-06-05 08:49 signoles Assigned To => virgile
2015-06-05 08:49 signoles Status new => assigned
2015-06-05 16:13 yakobowski Assigned To virgile => yakobowski
2015-06-05 16:15 yakobowski Relationship added related to 0002117
2015-06-08 13:12 yakobowski Note Added: 0005933
2015-06-08 18:56 Ian Note Added: 0005934
2015-06-08 21:21 yakobowski Note Added: 0005935
2015-06-08 21:21 yakobowski Status assigned => resolved
2015-06-08 21:21 yakobowski Resolution open => fixed
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker