#ifndef _max_h
#define _max_h
/*
 frama-c -jessie-analysis -jessie-int-model exact -jessie-gui max.c
 ======================================================================================
 DESCRIPTION:
  Returns the greater of a and b.
  The comparison uses operator< (b<a) for the first version, and comp for the second.


 Parameters:
  a, b:
   Items to compare. T is any type supporting copy constructions and comparisons with
   operator<.
  Return value:
   The greater of its two arguments

 Complexity:
  Constant
 ======================================================================================
*/

/*@
 ensures \result >= a && \result >= b;
  ensures \result == a || \result == b;
*/
int max ( int a, int b );

#endif