// @(#)$Id: make_ratl.lh,v 1.7 1997/06/03 20:30:13 leavens Exp $
typedef int *ratl;
extern ratl make_ratl(int n, int d) throw();
//@ behavior {
//@   requires d > 0;
//@   ensures assigned(result, post) /\ size(locs(result)) = 2
//@           /\ (result[0])' = n /\ (result[1])' = d
//@           /\ fresh(result[0], result[1]);
//@ }

[Index]

HTML generated using lcpp2html.