Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 204
    • Issues 204
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2559
Closed
Open
Created May 28, 2021 by Karine EM@karineek

No support for complex numbers via the keyword _Complex

Steps to reproduce the issue

Expected behaviour

Frama-c does not support complex numbers via the keyword _Complex for C code. See here: https://gcc.gnu.org/onlinedocs/gcc-4.1.2/gcc/Complex.html

Actual behaviour

When running this code:

float _Complex f;
int  main () { }

Frama-c returns an error:

[kernel] Parsing test12.c (with preprocessing) [kernel] test12.c:1:
   syntax error:
   Location: line 1, between columns 6 and 15, before or at token: f
   1     float _Complex f;
         ^^^^^^^^^^^^^^^^^
   2     int main () { }
[kernel] Frama-C aborted: invalid user input.

Contextual information

  • Frama-C installation mode: Opam
  • Frama-C version: Frama-C version (as reported by frama-c -version) 22.0 (Titanium)
  • Plug-in used: -eva
  • OS name: Ubuntu
  • OS version: 18

Additional information (optional)

We use Frama-c to automatically analyse code from llvm and gcc test-suites; some of the programs triggered this error message. I reduced the code but I can add the link to the original one.

Edited May 28, 2021 by Karine EM
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking