Destruction

[h0nzZik]

The rule for popBlock first calls all the destructors and then delete all objects:

rule <k> popBlock(IsException::Bool) => destructLocals(IsException) ~> unfoldBlockStack ~> deleteObjects(Locals) ~> exitRestrictBlock(Locals) ~> updateScope ...</k>
          <local-addresses> Locals::Set </local-addresses>
          [structural]

The consequence is that a destructor of the object that is being destroyed can still access the objects that are already destroyed, without triggering an error:

extern "C" int printf(char const *, ...);

struct S {
	int *p;
	~S(){
		printf("p: %d\n", *p);
	}
};

int main() {
	S s;
	int x = 1;
	s.p = &x;
	// x goes out of scope
	// s goes out of scope
}

That is probably a bug. If x is in a nested block, the execution gets stuck as expected:

int main() {
	S s;
	{
		int x = 1;
		s.p = &x;
		// x goes out of scope
	}
	// s goes out of scope
}

[h0nzZik]

Fixed in #564