Bug in example?

[Finii]

We have this code:

gcc-invariant-plugin/test/test.cpp

Lines 24 to 30 in 207d9e5

	void push(int value)
	[[pre: !full()]]
	[[post: top == old_top + 1]]
	{
	data[top++] = value;
	old_top = top;
	}

Will this not always trigger the post condition check, because, well, line 26 and 29 directly contradict?
Maybe lines 28 and 29 have to be swapped?

[GavinRay97]

Huh, logically thinking about it, I think you should be right, but if I run it, it does not trigger the check.

We can experiment with Contracts feature in Godbolt using GCC latest branch:

• https://gcc.godbolt.org/z/vK5xPT3Th

It looks like the [[post: ]] contract has been stripped, if I right-click in Godbolt and press Reveal linked code I get nothing for push().

However, you can see it works for pop(), and that if we change the condition for pop() we do get a contract violation:

[[post: top == old_top - 42]]

Doing the same for push does nothing:

[[post: top == old_top + 2]]

Wonder if it's worth bringing up on the mailing list about, or maybe there's a more obvious reason why it's being stripped?

[Finii]

Hmm, this is super strange. I played around with it a bit and it breaks in various combinations that seem to be not related.

For example, staring with your godbold

1. Simplify line 25 to be always false (Contract violation shown)
2. Change return type of push from void to int: Violation vanishes ??!

And while the original 'problem' with line 16 is visible above (the line is white, so no code generated for it), line 25 HAS code associated with it (yellowish bg color) (Stack::pop() [clone .post])

Ah I see...

If we get rid of the warning (i.e. put a return statement in push() we DO see the contract violation again.
And we do see it before, but only in the return value, just the message is missing in my example above:

Yes, I would bring this up on the list (I do not know of any list ;).

[Finii]

Ah ha!

post conditions seem to be only checked for functions returning something.
If you make pop() returning nothing its post condition is also ignored:

[GavinRay97]

post conditions seem to be only checked for functions returning something.

This seems like a pretty big gotcha that might be well to note somewhere, thank you for discovering this!