]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /* |
28bf4b0b | 2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001. |
885824d3 | 3 | ** See ../LICENSE for license information. |
4 | ** | |
5 | */ | |
6 | ||
28bf4b0b | 7 | typedef struct { |
885824d3 | 8 | ltoken name; |
9 | /*@null@*/ lclTypeSpecNode typespec; | |
10 | declaratorNode declarator; | |
11 | globalList globals; | |
12 | varDeclarationNodeList inits; | |
13 | letDeclNodeList lets; | |
14 | /*@null@*/ lclPredicateNode checks; | |
15 | /*@null@*/ lclPredicateNode require; | |
16 | /*@null@*/ modifyNode modify; | |
17 | /*@null@*/ lclPredicateNode ensures; | |
18 | /*@null@*/ lclPredicateNode claim; | |
19 | qual special; | |
20 | } *fcnNode; | |
21 | ||
22 | extern void fcnNode_free (/*@null@*/ /*@only@*/ fcnNode p_f); | |
23 | extern /*@only@*/ cstring fcnNode_unparse (/*@null@*/ fcnNode p_f); |