ultimate
ultimate copied to clipboard
Fix CDT parser include file handling and support recursion for includes
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.
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
andCACSL2BoogieTranslator
) and must be fixed (e.g. parsing global variable from an include file). - [x] Path separator literal is currently platform specific and should be automatically converted to a fixed literal, so that settings remain platform independent.
- [x] Include paths are currently absolute directory paths and it would be desirable if relative paths were also possible.
- [x] 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.