using real function ( \max, \min, \abs ) instead of integer one in function contract
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.