Kunjian Song

> and what exactly is the error? It should be verification failed, not verification successful. As A's member is not initialized in this case.

Because D's constructor didn't explicitly call `A(x)` in `D(int x) : B(x), C(x) {}` - this is basically equivalent to `D(int x) : A(), B(x), C(x) {}`. In this diamond...

Because B and C inherit A via virtual inheritance, and they are not the most derived class in this hierarchy.

> What's preventing you from implementing the rules you just explained? looking for a more efficient and elegant way to get "most_derived" information from clang... My conjecture is that clang...

Also, if we were to mark a virtual base and add the "most_derived" flag in its derived classes, it would be similar to the algorithm being used in the old...

This issue is blocked by https://github.com/esbmc/esbmc/issues/940. The `most_derived` flag relies on the correct execution order of constructors and destructors.

This issue is covered by the umbrella issue https://github.com/esbmc/esbmc/issues/940. based on the analysis in 940, this is a feature that also failed in CBMC and the old ESBMC not a...

Here's a workaround of this problem on macOS: ### Step 1: Install [email protected]: Since solc v0.4.x does not work with boost 1.7, I encountered [this problem](https://github.com/ethereum/solidity/issues/7529). you'll need to instal...