Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[cpp-clang] Don't parse fields for forward declarations.
Previously, esbmc would try to parse fields of forward declarations. Consider this code: ```cpp class a; // #1 class b; // #2 class a { // #3 b *c; }; class b : a {}; // #4 ``` When parsing #1, clang would resolve the actual definition for us. This means that we would skip ahead to #3 and try to parse the fields of `a`. When doing this, we will encounter `b` and try to get a type for it. This will ultimately fail, because we are still defining `a`, but `b` extends `a` and so `a` must be a _complete_ type which it is not at that point. We can avoid this problem by _not_ continuing to parse fields if the declaration is not a complete one. When now parsing #1, we would not skip ahead to #3 anymore. Similarly, when parsing #2, we would not skip ahead to #4 anymore. There is still a slight problem: when parsing #3 we would however still have a problem. We would try to get a type for `b` again, which would then fail again, because `a` is not yet complete. This problem is easily solved, by not recording structs in the context if we already have a symbol there for it.
- Loading branch information