--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on March 2009 ---
Hello, I have following code: === //@ ensures \result > 0 && \result < 4294967295; unsigned int f(void) { return 10; } void main(void) { unsigned int a, b, r; a = f(); b = f(); //@ assert a > 0 && b > 0; r = a % b; //@ assert r < b; } === With Alt-Ergo, I cannot prove "assert r < b" while this property seems obvious to me as "r = a % b". Is this a limitation of Alt-Ergo (Alt-Ergo does not know about modulo mathematical properties) or am I missing something (e.g. Frama-C works on mathematical integers which are different from unsigned int)? Yours, david