]> andersk Git - splint.git/blob - src/Headers/exprNode.h
Fixed state clauses. Added obvious loop exec checking.
[splint.git] / src / Headers / exprNode.h
1 /*
2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
3 ** See ../LICENSE for license information.
4 **
5 */
6 /*
7 ** exprNode.h
8 */
9
10 # ifndef EXPRNODE_H
11 # define EXPRNODE_H
12
13 /*
14 ** expression Nodes:
15 **
16 **     ctype typ --- type of expression
17 **
18 **     union _val
19 **      { long    ival;
20 **        char    cval;
21 **        double  fval;
22 **        cstring sval;
23 **      }   *val --- value, if known.  if unknown, val = (_val *)0
24 **
25 **     storeRef sref --- storage referred to by expression, of storeRef_null
26 **
27 **     cstring  etext --- to get nice error messages, punt for now!
28 */
29
30 /* in exprNode_type: typedef struct _exprNode *exprNode; */
31
32 typedef enum 
33
34   XPR_PARENS,     XPR_ASSIGN,  XPR_CALL,     XPR_EMPTY,    XPR_VAR, 
35   XPR_OP,         XPR_POSTOP,  XPR_PREOP,    XPR_SIZEOFT,  XPR_SIZEOF, XPR_ALIGNOFT, XPR_ALIGNOF,
36   XPR_OFFSETOF,   XPR_CAST,    XPR_FETCH,    XPR_VAARG,    XPR_ITER,  
37   XPR_FOR,        XPR_FORPRED, XPR_GOTO,     XPR_CONTINUE, XPR_BREAK, 
38   XPR_RETURN,     XPR_NULLRETURN, XPR_COMMA, XPR_COND,     XPR_IF,  XPR_IFELSE,
39   XPR_DOWHILE,    XPR_WHILE,   XPR_STMT,     XPR_STMTLIST, XPR_SWITCH,
40   XPR_INIT,       XPR_FACCESS, XPR_ARROW,    XPR_CONST,    XPR_STRINGLITERAL, 
41   XPR_NUMLIT,     XPR_BODY,    XPR_NODE,     XPR_ITERCALL, XPR_TOK,
42   XPR_WHILEPRED,  XPR_CASE,    XPR_FTCASE,   XPR_DEFAULT,  XPR_FTDEFAULT,
43   XPR_BLOCK,      XPR_INITBLOCK, XPR_LABEL
44 } exprKind; 
45
46 typedef struct 
47 {
48   /*@only@*/ qtype q;
49   /*@only@*/ cstringList field;
50 } *exprOffsetof;
51
52 typedef struct 
53 {
54   /*@only@*/ exprNode a;
55   /*@only@*/ exprNode b;
56 } *exprPair;
57
58 typedef struct
59 {
60   /*@only@*/ exprNode pred;
61   /*@only@*/ exprNode tbranch;
62   /*@only@*/ exprNode fbranch;
63 } *exprTriple;
64
65 typedef struct
66 {
67   /*@dependent@*/ /*@observer@*/ uentry sname;
68   /*@only@*/    exprNodeList args;
69   /*@only@*/    exprNode body;
70   /*@dependent@*/ /*@observer@*/ uentry ename;
71 } *exprIter;
72
73 typedef struct
74 {
75   /*@only@*/ exprNode fcn;
76   /*@only@*/ exprNodeList args;
77 } *exprCall;
78
79 typedef struct
80 {
81   /*@dependent@*/ /*@exposed@*/ uentry iter;
82   /*@only@*/   exprNodeList args;
83 } *exprIterCall;
84
85 typedef struct
86 {
87   /*@only@*/ exprNode a;
88   /*@only@*/ exprNode b;
89   lltok      op;
90 } *exprOp;
91
92 typedef struct
93 {
94   /*@only@*/ exprNode rec;
95   /*@only@*/ cstring  field;
96 } *exprField;
97
98 typedef struct
99 {
100   /*@only@*/ exprNode a;
101   lltok      op;
102 } *exprUop;
103
104 typedef struct
105 {
106   /*@only@*/ exprNode exp;
107              lltok    tok;
108              qtype    q;
109 } *exprCast;
110
111 typedef struct
112 {
113   /*@only@*/ exprNode exp;
114              idDecl   id;
115 } *exprInit;
116
117 typedef /*@null@*/ union
118 {
119   cstring literal;
120   cstring id;
121   lltok *tok;
122   qtype qt;    /* sizeof(type) */
123   /* use for any 2-operator (comma, arrayFetch, case, stmt) */
124   exprPair pair; 
125   exprOp op;    /* pair + operator */
126   exprUop uop;
127   exprInit init;
128   exprIter iter;
129   exprCall call;
130   exprIterCall itercall;
131   exprCast cast;
132   exprNode single;
133   exprField field;
134   exprTriple triple; /* ifelse, ternary op, for pred */
135   exprOffsetof offset;
136 } *exprData;
137
138 /*@constant null exprData exprData_undefined; @*/
139 # define exprData_undefined  ((exprData) NULL)
140
141 struct s_exprNode
142 {
143   bool isJumpPoint BOOLBITS; /* expr can be reached non-sequentially */
144   bool canBreak BOOLBITS;    /* expr can break (has break, continue) */
145   bool mustBreak BOOLBITS;
146
147   ctype typ;
148   exitkind exitCode;    
149
150   multiVal val;
151   /*@exposed@*/ sRef sref;
152   sRefSet uses;   /* sRef's used by this expression */
153   sRefSet sets;   /* sRef's set by this expression */
154   sRefSet msets;  /* sRef's possibly set (implicit out params, etc.) */
155
156   guardSet guards;
157   exprKind kind;
158
159   fileloc loc;
160   /*@relnull@*/ exprData edata;
161   cstring etext;
162   /*@notnull@*/   constraintList requiresConstraints;
163   /*@notnull@*/ constraintList ensuresConstraints;
164   
165   /*
166   ** These two are used only for boolean expressions, 
167   ** they store the ensures constraints for the true and false cases
168   */
169
170   /*@notnull@*/ constraintList trueEnsuresConstraints;
171   /*@notnull@*/ constraintList falseEnsuresConstraints;
172 } ;
173
174 /*@constant null exprNode exprNode_undefined; @*/
175 # define exprNode_undefined ((exprNode)NULL)
176
177 extern /*@falsenull@*/ bool exprNode_isDefined (exprNode p_e) /*@*/ ;
178 extern /*@unused@*/ /*@truenull@*/ bool exprNode_isUndefined (exprNode p_e) /*@*/ ;
179 extern /*@truenull@*/ bool exprNode_isError (exprNode p_e) /*@*/ ;
180
181 # define exprNode_isDefined(e)        ((e) != exprNode_undefined)
182 # define exprNode_isUndefined(e)      ((e) == exprNode_undefined)
183 # define exprNode_isError(e)          ((e) == exprNode_undefined)
184
185 extern /*@dependent@*/ /*@exposed@*/ guardSet 
186   exprNode_getGuards (/*@sef@*/ exprNode p_e) /*@*/ ;
187 # define exprNode_getGuards(e) \
188   (exprNode_isDefined(e) ? (e)->guards : guardSet_undefined)
189
190 extern ctype exprNode_getType (/*@sef@*/ exprNode p_e) /*@*/ ;
191 # define exprNode_getType(e) \
192   (exprNode_isDefined(e) ? (e)->typ : ctype_unknown)
193
194 extern /*@unused@*/ /*@falsenull@*/ bool exprNode_isInParens (/*@sef@*/ exprNode p_e) /*@*/ ;
195 # define exprNode_isInParens(e) \
196   (exprNode_isDefined(e) && (e)->kind == XPR_PARENS)
197
198 extern bool exprNode_isStringLiteral (/*@sef@*/ exprNode p_e) /*@*/ ;
199 # define exprNode_isStringLiteral(e) \
200   (exprNode_isDefined(e) && (e)->kind == XPR_STRINGLITERAL)
201
202 extern /*@unused@*/ bool exprNode_knownIntValue (/*@sef@*/ exprNode p_e) /*@*/ ;
203 # define exprNode_knownIntValue(e) \
204   (exprNode_isDefined(e) && multiVal_isInt (exprNode_getValue (e)))
205
206 extern /*@unused@*/ bool exprNode_knownStringValue (/*@sef@*/ exprNode p_e) /*@*/ ;
207 # define exprNode_knownStringValue(e) \
208   (exprNode_isDefined(e) && multiVal_isString (exprNode_getValue (e)))
209
210 extern bool exprNode_hasValue (/*@sef@*/ exprNode p_e) /*@*/ ;
211 # define exprNode_hasValue(e) \
212   (exprNode_isDefined(e) && multiVal_isDefined (exprNode_getValue (e)))
213
214 extern /*@exposed@*/ multiVal exprNode_getValue (exprNode p_e) /*@*/ ;
215 extern long exprNode_getLongValue (exprNode p_e) /*@*/ ;
216
217 extern /*@observer@*/ cstring exprNode_unparseFirst (exprNode p_e) /*@*/ ;
218 extern /*@observer@*/ guardSet exprNode_getForGuards (exprNode p_pred) /*@*/ ;
219 extern bool exprNode_loopMustExec (exprNode p_forPred) /*@*/ ;
220
221 extern bool exprNode_isNullValue (exprNode p_e) /*@*/ ;
222 extern /*@exposed@*/ sRef exprNode_getSref (exprNode p_e) /*@*/ ;
223 extern /*@exposed@*/ uentry exprNode_getUentry (exprNode p_e) 
224    /*@globals internalState@*/ ;
225 extern void exprNode_produceGuards (exprNode p_pred) /*@modifies p_pred@*/ ;
226
227 extern /*@observer@*/ fileloc exprNode_loc (exprNode p_e) /*@*/ ;
228 extern /*@observer@*/ fileloc exprNode_getLoc (exprNode p_e) /*@*/ ;
229 # define exprNode_getLoc exprNode_loc
230
231 extern exprNode
232   exprNode_charLiteral (char p_c, cstring p_text, /*@only@*/ fileloc p_loc) /*@*/ ;
233 extern /*@observer@*/ exprNode exprNode_makeMustExit (void) /*@*/ ;
234 extern exprNode 
235   exprNode_cond (/*@keep@*/ exprNode p_pred, /*@keep@*/ exprNode p_ifclause, 
236                  /*@keep@*/ exprNode p_elseclause) /*@*/ ;
237 extern exprNode exprNode_makeError(void) /*@*/ ;
238
239 extern exprNode exprNode_makeInitBlock (lltok p_brace, /*@only@*/ exprNodeList p_inits) /*@*/ ;
240
241 extern exprNode exprNode_functionCall (/*@only@*/ exprNode p_f, 
242                                        /*@only@*/ exprNodeList p_args) /*@*/ ;
243 extern /*@notnull@*/ exprNode 
244   exprNode_fromIdentifier (/*@observer@*/ uentry p_c) /*@globals internalState@*/ ;
245 extern exprNode exprNode_fromUIO (cstring p_c) /*@globals internalState@*/ ;
246 extern exprNode exprNode_fieldAccess (/*@only@*/ exprNode p_s, 
247                                       /*@only@*/ lltok p_dot,
248                                       /*@only@*/ cstring p_f) /*@*/ ;
249
250 extern exprNode exprNode_arrowAccess (/*@only@*/ exprNode p_s,
251                                       /*@only@*/ lltok p_arrow,
252                                       /*@only@*/ cstring p_f) /*@*/ ;
253
254 extern exprNode exprNode_postOp (/*@only@*/ exprNode p_e, /*@only@*/ lltok p_op) 
255           /*@modifies p_e@*/ ;
256 extern exprNode exprNode_preOp (/*@only@*/ exprNode p_e, /*@only@*/ lltok p_op) /*@*/ ;
257 extern exprNode exprNode_addParens (/*@only@*/ lltok p_lpar, /*@only@*/ exprNode p_e) /*@*/ ;
258 extern exprNode exprNode_offsetof (/*@only@*/ qtype p_qt, /*@only@*/ cstringList p_s) /*@*/ ;
259 extern exprNode exprNode_sizeofType (/*@only@*/ qtype p_qt) /*@*/ ;
260 extern exprNode exprNode_sizeofExpr (/*@only@*/ exprNode p_e) /*@*/ ;
261 extern exprNode exprNode_alignofType (/*@only@*/ qtype p_qt) /*@*/ ;
262 extern exprNode exprNode_alignofExpr (/*@only@*/ exprNode p_e) /*@*/ ;
263 extern exprNode 
264   exprNode_op (/*@only@*/ exprNode p_e1, /*@keep@*/ exprNode p_e2, /*@only@*/ lltok p_op) /*@*/ ;
265 extern exprNode 
266   exprNode_assign (/*@only@*/ exprNode p_e1, /*@only@*/ exprNode p_e2, /*@only@*/ lltok p_op) ;
267 extern exprNode
268   exprNode_arrayFetch (/*@only@*/ exprNode p_e1, /*@only@*/ exprNode p_e2) 
269   /*@modifies p_e1, p_e2@*/ ;
270
271 extern void exprNode_free (/*@only@*/ exprNode p_e) ;
272 extern exprNode
273   exprNode_vaArg (/*@only@*/ lltok p_tok, /*@only@*/ exprNode p_arg, /*@only@*/ qtype p_qt) 
274   /*@globals internalState@*/ ;
275
276 /*
277 ** Has surrounding quotes.
278 */
279
280 extern exprNode 
281   exprNode_stringLiteral (/*@only@*/ cstring p_t, /*@only@*/ fileloc p_loc) /*@*/ ;
282
283 extern /*@only@*/ exprNode
284   exprNode_wideStringLiteral (/*@only@*/ cstring p_t, /*@only@*/ fileloc p_loc) /*@*/ ;
285
286 /*
287 ** No surrounding quotes.
288 */
289
290 extern exprNode 
291   exprNode_rawStringLiteral (/*@only@*/ cstring p_t, /*@only@*/ fileloc p_loc) /*@*/ ;
292
293 extern exprNode exprNode_comma (/*@only@*/ exprNode p_e1, /*@only@*/ exprNode p_e2)  /*@*/ ;
294 extern exprNode exprNode_labelMarker (/*@only@*/ cstring p_label);
295 extern exprNode 
296   exprNode_notReached (/*@returned@*/ exprNode p_stmt);
297
298 extern
299 exprNode exprNode_caseMarker (/*@only@*/ exprNode p_test, bool p_fallThrough) /*@*/ ;
300
301 extern exprNode exprNode_concat (/*@only@*/ exprNode p_e1, /*@only@*/ exprNode p_e2);
302 extern exprNode exprNode_createTok (/*@only@*/ lltok p_t) /*@*/ ;
303 extern exprNode exprNode_statement (/*@only@*/ exprNode p_e, /*@only@*/ lltok p_t);
304 extern exprNode exprNode_makeBlock (/*@only@*/ exprNode p_e);
305 extern exprNode exprNode_if (/*@only@*/ exprNode p_pred, /*@only@*/ exprNode p_tclause);
306 extern exprNode 
307   exprNode_ifelse (/*@only@*/ exprNode p_pred, /*@only@*/ exprNode p_tclause, 
308                    /*@only@*/ exprNode p_eclause);
309 extern exprNode exprNode_switch (/*@only@*/ exprNode p_e, /*@only@*/ exprNode p_s);
310 extern exprNode exprNode_while (/*@keep@*/ exprNode p_t, /*@keep@*/ exprNode p_b);
311 extern exprNode exprNode_doWhile (/*@only@*/ exprNode p_b, /*@only@*/ exprNode p_t);
312 extern /*@notnull@*/ /*@only@*/ exprNode exprNode_goto (/*@only@*/ cstring p_label);
313 extern exprNode exprNode_continue (/*@only@*/ lltok p_l, int p_qcontinue);
314 extern exprNode exprNode_break (/*@only@*/ lltok p_l, int p_bqual);
315 extern exprNode exprNode_nullReturn (/*@only@*/ lltok p_t);
316 extern exprNode exprNode_return (/*@only@*/ exprNode p_e);
317 extern /*@dependent@*/ /*@observer@*/ cstring 
318 exprNode_unparse (/*@temp@*/ exprNode p_e) /*@*/ ; 
319
320 extern bool exprNode_isCharLit (exprNode p_e) /*@*/ ;
321 extern bool exprNode_isNumLit (exprNode p_e) /*@*/ ;
322
323 extern exprNode 
324   exprNode_makeInitialization (/*@only@*/ idDecl p_t, /*@only@*/ exprNode p_e);
325
326 exprNode exprNode_makeEmptyInitialization (/*@only@*/ idDecl p_t) ;
327
328 extern bool exprNode_isInitializer (exprNode p_e) /*@*/ ;
329
330 extern bool exprNode_matchType (ctype p_expected, exprNode p_e);
331
332 extern /*@notnull@*/ /*@only@*/ exprNode 
333   exprNode_defaultMarker (/*@only@*/ lltok p_def, bool p_fallThrough);
334
335 extern exprNode 
336   exprNode_iter (/*@observer@*/ uentry p_name, /*@only@*/ exprNodeList p_alist, 
337                  /*@only@*/ exprNode p_body, /*@observer@*/ uentry p_end);
338 extern exprNode exprNode_iterId (/*@observer@*/ uentry p_c);
339 extern            exprNode exprNode_iterExpr (/*@returned@*/ exprNode p_e);
340 extern exprNode exprNode_iterNewId (/*@only@*/ cstring p_s);
341 extern exprNode 
342   exprNode_iterStart (/*@observer@*/ uentry p_name, /*@only@*/ exprNodeList p_alist);
343 extern exprNode 
344   exprNode_numLiteral (ctype p_c, /*@temp@*/ cstring p_t, 
345                        /*@only@*/ fileloc p_loc, long p_val); 
346 extern void exprNode_initMod (void) /*@modifies internalState@*/ ;
347 extern exprNode exprNode_for (/*@keep@*/ exprNode p_inc, /*@keep@*/ exprNode p_body);
348 extern exprNode 
349   exprNode_forPred (/*@only@*/ exprNode p_init, 
350                     /*@only@*/ exprNode p_test, /*@only@*/ exprNode p_inc);
351 extern exprNode 
352   exprNode_floatLiteral (double p_d, ctype p_ct, 
353                          cstring p_text, /*@only@*/ fileloc p_loc);
354 extern /*@notnull@*/ exprNode exprNode_createId (/*@observer@*/ uentry p_c);
355 extern /*@notnull@*/ exprNode exprNode_makeConstantString (/*@temp@*/ cstring p_c, /*@only@*/ fileloc p_loc) /*@*/ ;
356 extern exprNode exprNode_cast (/*@only@*/ lltok p_tok, /*@only@*/ exprNode p_e, /*@only@*/ qtype p_q);
357 extern bool exprNode_matchLiteral (ctype p_expected, exprNode p_e);
358 extern void exprNode_checkUseParam (exprNode p_current);
359 extern void exprNode_checkSet (exprNode p_e, /*@exposed@*/ sRef p_s);
360 extern void exprNode_checkMSet (exprNode p_e, /*@exposed@*/ sRef p_s);
361 extern exprNode exprNode_checkExpr (/*@returned@*/ exprNode p_e);
362 extern bool exprNode_mustEscape (exprNode p_e);
363 extern bool exprNode_errorEscape (exprNode p_e);
364 extern bool exprNode_mayEscape (exprNode p_e);
365 extern exprNode exprNode_whilePred (/*@only@*/ exprNode p_test);
366 extern exprNode 
367   exprNode_updateLocation (/*@returned@*/ exprNode p_e, /*@temp@*/ fileloc p_loc);
368 extern void exprNode_freeShallow (/*@only@*/ exprNode p_e);
369 extern void exprNode_destroyMod (void) /*@modifies internalState@*/ ;
370 extern bool exprNode_isAssign (exprNode p_e) /*@*/ ;
371
372 /* added 8-15-00
373    by DRL */
374 extern /*@observer@*/ fileloc exprNode_getfileloc (exprNode p_e) ;
375
376 /*@-exportlocal@*/
377 extern bool exprNode_isDefaultMarker (exprNode p_e) /*@*/ ;
378 extern bool exprNode_isCaseMarker (exprNode p_e) /*@*/ ;
379 extern bool exprNode_isLabelMarker (exprNode p_e) /*@*/ ;
380 /*@=exportlocal@*/
381
382 extern /*@only@*/ exprNode exprNode_combineLiterals (/*@only@*/ exprNode p_e, /*@only@*/ exprNode p_rest) ;
383
384 extern /*@only@*/ fileloc exprNode_getNextSequencePoint (exprNode p_e) ;
385
386 /*drl 01-20-2001*/
387 exprNode exprNode_createNew(ctype p_c);
388
389 /* drl 07-25-01 */
390 bool exprNode_isInitBlock (exprNode p_e);
391
392 # else
393 # error "Multiple include"
394 # endif
This page took 0.071387 seconds and 5 git commands to generate.