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 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2552

Closed
Open
Created May 02, 2021 by marce9@marce9

Errors when trying to analyze programs including MSVC headers

Hi, We are trying to slice the simple program tst3.cpp (included tst3.cpp). The execution command is: frama-c tst3.cpp -slice-calls g -slicing-level 1 -slicing-keep-annotations -then-on 'Slicing export' -print -ocode output.cpp The slicing succeeds and the output is: tst3_no_includes_execution_success

However, when adding 2 includes <stdio.h> & <string.h> the slicing fails with the following output: tst3_with_includes_execution_failure

Moreover, we keep facing failures when trying to slice simple programs with the MinGW's GCC compiler and headers. For example, for tried execution the following command:

frama-c -cpp-command 'x86_64-w64-mingw32-gcc -C -E -I /usr/x86_64-w64-mingw32/include' -cpp-frama-c-compliant tst3.cpp -slice-calls g -slicing-level 1 -slicing-keep-annotations -then-on 'Slicing export' -print -ocode output.cpp

The errors range from "invalid user input" on header files, to incompatible arch mode (32, 64 bit).

Hope to receive help with the right way of executing things, including the right commands with the right parameters, how to use MinGW in order to slice visual-C++ code (MSVC), etc.

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