    Add(x,y):
       Assert( x >= 0 && y>= 0 )
        z = x + y
        Assert( z >= x && z >= y )
        return z

There’s definitely smarter ways to do this, but in practice there is always some way to encode the properties you care about in ways that your assertions will be violated. If you can’t observe a violation, it’s not a violation https://en.wikipedia.org/wiki/Identity_of_indiscernibles

▲ 16 hours ago | parent | next [-]

[deleted]

▲ bluGill 15 hours ago | parent | prev [-]

In some languages overflow is asserted as a can't happen and so the optimizer will remove your checks

▲ appellations 13 hours ago | parent | next [-]

Best I can tell is that overflow is undefined behavior for signed ints in C/C++ so -O3 with gcc might remove a check that could only be true if UB occurred.

The compound predicate in my example above coupled with the fact that the compiler doesn’t reason about the precondition in the prior assert (y is non-negative) means this specific example wouldn’t be optimized away, but bluGill does have a point.

An example of an assert that might be optimized away:

    int addFive(int x) {
        int y = x + 5;
        assert(y >= x);
        return y;
    }

	▲	uecker 9 hours ago \| parent \| next [-]
		Yes, you can not meaningfully assert anything after UB in C/C++. But you can let the compiler add the trap for overflow -fsanitize=signed-integer-overflow -sanitize-trap=all, or you could also write your assertion in a way where it does not rely on the result (e.g. ckd_add), or you use "volatile" to write in a way the compiler is not allowed to assume anything.
	▲	comex 11 hours ago \| parent \| prev [-]
		Clang is a bit smarter than GCC here (for some definition of 'smart') and does optimize the original version: https://gcc.godbolt.org/z/3Y4aheG6x

▲ appellations 13 hours ago | parent | prev [-]

Care to share a language where the compiler infers the semantic meaning of asserts and optimizes them away? I’ve never heard of this optimization.

	▲	mrkeen 8 hours ago \| parent \| next [-]
		C. This is a great thread: https://mastodon.social/@regehr/113821964763012870 (That was one of my texts at uni)
	▲	MindSpunk 10 hours ago \| parent \| prev [-]
		Signed overflow is UB in C/C++ and several compilers will skip explicit overflow checks as a result. See: https://godbolt.org/z/WehcWj3G5