// @(#)$Id: time.lh,v 1.11 1997/07/31 04:02:27 leavens Exp $

// the following defines time_t
#include "types.lh"

//@ spec volatile time_t system_clock;

extern time_t time(time_t * tloc) throw();
//@ behavior {
//@   requires allocated(tloc, pre);
//@   modifies *tloc;
//@   ensures result = system_clock^ /\ tloc' = system_clock^;
//@ also
//@   requires isNull(tloc);
//@   ensures result = system_clock^;
//@ }

[Index]

HTML generated using lcpp2html.