ID0000655: **This issue was created automatically from Mantis Issue 655. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0000655 | Frama-C | Kernel > ACSL implementation | public | 2010-12-25 | 2014-02-12 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | evdenis | **Assigned To** | virgile | **Resolution** | fixed | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 | ### Description : /*@ @ ensures \result == \max( a, b ); @ ensures \result != \min( a, b ); @ ensures a == \abs( a ); @*/ unsigned int max( unsigned int a, unsigned int b ) { int i = a > b ? a : b; //@ assert i == \max( a, b ); return i; } Jessie output: uint32 max(uint32 a, uint32 b) behavior default: ensures (C_8 : ((C_9 : (\result == \real_max(a, b))) && ((C_11 : (\result != \real_min(a, b))) && (C_12 : (a == \real_abs(a)))))); I don't know exactly is it a bug or a feature. ## Attachments - [max.c](/uploads/f369fbe09713900271c3103971ae67b4/max.c)