Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix CDT parser include file handling and support recursion for includes #639

Draft
wants to merge 8 commits into
base: dev
Choose a base branch
from

Conversation

bahnwaerter
Copy link
Member

@bahnwaerter bahnwaerter commented Jun 22, 2023

This patch adds a new CDT parser option to support recursive adding of include files. With this option, include files can be added recursively from subdirectories of include paths as well. This patch also fixes the existing CDT parser include file handling and adds a CDT parser test suite. The test suite implements various test cases intended to test the parsing of C programs that include header files. Each test case modifies the CDT parser settings for an automatic test setup to check the different include path configurations.

With this option, include files can be added recursively from
subdirectories of include paths as well.
This test suite implements various test cases intended to test
the parsing of C programs that include header files. Each test
case modifies the CDT parser settings for an automatic test setup
to check the different include path configurations.
@bahnwaerter
Copy link
Member Author

bahnwaerter commented Jun 23, 2023

Note that the fix for the CDT parser include handling in this patch still has some limitations and missing features that still need to be improved to complete all test cases successfully:

  • Handling of multiple CDT translation units is currently broken (somewhere in the CDTParser and CACSL2BoogieTranslator) and must be fixed (e.g. parsing global variable from an include file).
  • Path separator literal is currently platform specific and should be automatically converted to a fixed literal, so that settings remain platform independent.
  • Include paths are currently absolute directory paths and it would be desirable if relative paths were also possible.
  • Resolve and parse local include file (header.h) specified by #include "header.h" automatically without explicitly adding the local program folder to the local include path.
  • Add command line option -I for one or several include paths to be option-compatible with standard parsers like Clang or GCC.

@bahnwaerter bahnwaerter self-assigned this Oct 5, 2023
This patch fixes the C preprocessor to support the parsing and
substitution of the following macros:

  - #define
  - #undef
  - #if
  - #ifdef
  - #ifndef
  - #elif
  - #else
  - #endif
  - #error

Note that ACSL expressions cannot contain macros, as these are in
comments where parsing and substitution is not possible.
@@ -0,0 +1,34 @@
//#Unafe
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

//#Unsafe

Copy link
Member Author

@bahnwaerter bahnwaerter Nov 17, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for pointing out the invalid program correctness specifier.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants