Project

General

Profile

Bug #9546

Frama-C (CIL) for GCC does not behave like GCC when casting ternary operators

Added by Evgeny Novikov 5 months ago. Updated 5 months ago.

Status:
Closed
Priority:
Urgent
Start date:
03/15/2019
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

For instance, for the following program:

void func(int arg)
{
        (long unsigned int)( arg  == 0 ? -1 : 1);
}

Frama-C (CIL) issues the following error:
[kernel] Parsing test.c (with preprocessing)
[kernel] test.c:4:1: User Error: 
  cannot cast from void to unsigned long

  2     void func(int arg)
  3     {
  4             (long unsigned int)( arg  == 0 ? -1 : 1);
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  5     }
[kernel] User Error: skipping file test.c that has errors.
[kernel] Frama-C aborted: invalid user input.

when launched as follows:
toplevel.opt -no-autoload-plugins -no-findlib -machdep gcc_x86_64 test.c -print -print-lines -ocode test.cil.c

GCC can compile this code without any issues. You can read this discussion.


Related issues

Related to C Instrumentation Framework - Bug #9534: Incorrect printing of Linux BUILD_BUG_ONRejected03/13/2019

Actions
Blocks Klever - Bug #6629: Used CIL is outdatedClosed03/13/2019

Actions

History

#1

Updated by Evgeny Novikov 5 months ago

  • Blocks Bug #6629: Used CIL is outdated added
#2

Updated by Evgeny Novikov 5 months ago

  • Related to Bug #9534: Incorrect printing of Linux BUILD_BUG_ON added
#3

Updated by Mikhail Mandrykin 5 months ago

This is actually an old bug that was already fixed in Silicon (v14.0), but was somehow lost during the merge in b8012367. Fixed in f2445d34

#4

Updated by Evgeny Novikov 5 months ago

The fix works well! Merges do can bring strange issues, so, there is nothing surprising. Please, close the issue.

#5

Updated by Mikhail Mandrykin 5 months ago

  • Status changed from New to Closed

Also available in: Atom PDF