// @(#)$Id: linkage_declaration.lh,v 1.6 1997/06/03 20:30:12 leavens Exp $

extern "C" double ceil(double x);

extern "C" double floor(double x);
//@ behavior {
//@   ensures returns /\ x - 1 < result /\ result <= x;
//@ }

extern "C" {
  // @spec int seed_value;

  void srand(int seed);
  //@ behavior {
  //@   modifies seed_value;
  //@   ensures returns /\ assigned(seed_value, post) /\ seed_value' = seed;
  //@ }

  int rand();
  //@ behavior {
  //@   requires assigned(seed_value, pre);
  //@   ensures returns /\ 0 < result /\ result <= INT_MAX;
  //@ }
}

[Index]

HTML generated using lcpp2html.