Skip to content

protected variable not visible in contract in subclass

ID0002032: This issue was created automatically from Mantis Issue 2032. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002032 Frama-Clang Plug-in > clang public 2014-12-15 2015-02-15
Reporter Jochen Assigned To virgile Resolution duplicate
Priority normal Severity minor Reproducibility always
Platform frama-c-Neon-20140301+dev-stance OS - OS Version xubuntu-cfe13.10
Product Version - Target Version - Fixed in Version -

Description :

output:

Now output intermediate result 405.cpp:6:[kernel] user error: Cannot find field salary

The error message remains even if "salary" is made "public" in line 2. It disappears if the assigns clause in line 5 is deleted.

If "salary" is changed to "Employee::salary" in line 5 (contract), Frama-C aborts with the output:

framaCIRGen: SemaLookup.cpp:1622: bool clang::Sema::LookupQualifiedName(clang::LookupResult &, clang::DeclContext *, bool): Assertion `(!isa(LookupCtx) || LookupCtx->isDependentContext() || cast(LookupCtx)->isCompleteDefinition() || cast(LookupCtx)->isBeingDefined()) && "Declaration context must already be complete!"' failed. Aborted (core dumped)

Attachments

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information