]> andersk Git - splint.git/blame - src/Headers/exprNode.h
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Added support for omitted if clauses in conditionals, patch provided by peteran.
[splint.git] / src / Headers / exprNode.h
CommitLineData
885824d3 1/*
c0de361f 2** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
885824d3 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
32typedef 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,
1214340e 43 XPR_BLOCK, XPR_INITBLOCK,
44 XPR_LABEL
885824d3 45} exprKind;
46
28bf4b0b 47typedef struct
885824d3 48{
49 /*@only@*/ qtype q;
50 /*@only@*/ cstringList field;
51} *exprOffsetof;
52
28bf4b0b 53typedef struct
885824d3 54{
55 /*@only@*/ exprNode a;
56 /*@only@*/ exprNode b;
57} *exprPair;
58
28bf4b0b 59typedef struct
885824d3 60{
61 /*@only@*/ exprNode pred;
62 /*@only@*/ exprNode tbranch;
63 /*@only@*/ exprNode fbranch;
64} *exprTriple;
65
28bf4b0b 66typedef struct
885824d3 67{
68 /*@dependent@*/ /*@observer@*/ uentry sname;
69 /*@only@*/ exprNodeList args;
70 /*@only@*/ exprNode body;
71 /*@dependent@*/ /*@observer@*/ uentry ename;
72} *exprIter;
73
28bf4b0b 74typedef struct
885824d3 75{
76 /*@only@*/ exprNode fcn;
77 /*@only@*/ exprNodeList args;
78} *exprCall;
79
28bf4b0b 80typedef struct
885824d3 81{
82 /*@dependent@*/ /*@exposed@*/ uentry iter;
83 /*@only@*/ exprNodeList args;
84} *exprIterCall;
85
28bf4b0b 86typedef struct
885824d3 87{
88 /*@only@*/ exprNode a;
89 /*@only@*/ exprNode b;
90 lltok op;
91} *exprOp;
92
28bf4b0b 93typedef struct
885824d3 94{
95 /*@only@*/ exprNode rec;
96 /*@only@*/ cstring field;
97} *exprField;
98
28bf4b0b 99typedef struct
885824d3 100{
101 /*@only@*/ exprNode a;
102 lltok op;
103} *exprUop;
104
28bf4b0b 105typedef struct
885824d3 106{
107 /*@only@*/ exprNode exp;
108 lltok tok;
109 qtype q;
110} *exprCast;
111
28bf4b0b 112typedef struct
885824d3 113{
114 /*@only@*/ exprNode exp;
115 idDecl id;
116} *exprInit;
117
28bf4b0b 118typedef /*@null@*/ union
885824d3 119{
120 cstring literal;
121 cstring id;
80489f0a 122 lltok tok;
885824d3 123 qtype qt; /* sizeof(type) */
124 /* use for any 2-operator (comma, arrayFetch, case, stmt) */
125 exprPair pair;
126 exprOp op; /* pair + operator */
127 exprUop uop;
128 exprInit init;
129 exprIter iter;
130 exprCall call;
131 exprIterCall itercall;
132 exprCast cast;
133 exprNode single;
134 exprField field;
135 exprTriple triple; /* ifelse, ternary op, for pred */
136 exprOffsetof offset;
137} *exprData;
138
139/*@constant null exprData exprData_undefined; @*/
140# define exprData_undefined ((exprData) NULL)
141
28bf4b0b 142struct s_exprNode
885824d3 143{
144 bool isJumpPoint BOOLBITS; /* expr can be reached non-sequentially */
145 bool canBreak BOOLBITS; /* expr can break (has break, continue) */
146 bool mustBreak BOOLBITS;
147
148 ctype typ;
149 exitkind exitCode;
150
151 multiVal val;
152 /*@exposed@*/ sRef sref;
153 sRefSet uses; /* sRef's used by this expression */
154 sRefSet sets; /* sRef's set by this expression */
155 sRefSet msets; /* sRef's possibly set (implicit out params, etc.) */
156
157 guardSet guards;
158 exprKind kind;
159
160 fileloc loc;
161 /*@relnull@*/ exprData edata;
162 cstring etext;
ae133592 163 /*@notnull@*/ constraintList requiresConstraints;
bb25bea6 164 /*@notnull@*/ constraintList ensuresConstraints;
b7b694d6 165
166 /*
167 ** These two are used only for boolean expressions,
168 ** they store the ensures constraints for the true and false cases
169 */
170
bb25bea6 171 /*@notnull@*/ constraintList trueEnsuresConstraints;
172 /*@notnull@*/ constraintList falseEnsuresConstraints;
885824d3 173} ;
174
175/*@constant null exprNode exprNode_undefined; @*/
176# define exprNode_undefined ((exprNode)NULL)
177
0e41eb0e 178extern /*@falsewhennull@*/ bool exprNode_isDefined (exprNode p_e) /*@*/ ;
179extern /*@unused@*/ /*@nullwhentrue@*/ bool exprNode_isUndefined (exprNode p_e) /*@*/ ;
180extern /*@nullwhentrue@*/ bool exprNode_isError (exprNode p_e) /*@*/ ;
885824d3 181
182# define exprNode_isDefined(e) ((e) != exprNode_undefined)
183# define exprNode_isUndefined(e) ((e) == exprNode_undefined)
184# define exprNode_isError(e) ((e) == exprNode_undefined)
185
186extern /*@dependent@*/ /*@exposed@*/ guardSet
187 exprNode_getGuards (/*@sef@*/ exprNode p_e) /*@*/ ;
188# define exprNode_getGuards(e) \
189 (exprNode_isDefined(e) ? (e)->guards : guardSet_undefined)
190
191extern ctype exprNode_getType (/*@sef@*/ exprNode p_e) /*@*/ ;
192# define exprNode_getType(e) \
193 (exprNode_isDefined(e) ? (e)->typ : ctype_unknown)
194
0e41eb0e 195extern /*@unused@*/ /*@falsewhennull@*/ bool exprNode_isInParens (/*@sef@*/ exprNode p_e) /*@*/ ;
885824d3 196# define exprNode_isInParens(e) \
197 (exprNode_isDefined(e) && (e)->kind == XPR_PARENS)
198
28bf4b0b 199extern bool exprNode_isStringLiteral (/*@sef@*/ exprNode p_e) /*@*/ ;
885824d3 200# define exprNode_isStringLiteral(e) \
201 (exprNode_isDefined(e) && (e)->kind == XPR_STRINGLITERAL)
202
203extern /*@unused@*/ bool exprNode_knownIntValue (/*@sef@*/ exprNode p_e) /*@*/ ;
204# define exprNode_knownIntValue(e) \
205 (exprNode_isDefined(e) && multiVal_isInt (exprNode_getValue (e)))
206
207extern /*@unused@*/ bool exprNode_knownStringValue (/*@sef@*/ exprNode p_e) /*@*/ ;
208# define exprNode_knownStringValue(e) \
209 (exprNode_isDefined(e) && multiVal_isString (exprNode_getValue (e)))
210
211extern bool exprNode_hasValue (/*@sef@*/ exprNode p_e) /*@*/ ;
212# define exprNode_hasValue(e) \
213 (exprNode_isDefined(e) && multiVal_isDefined (exprNode_getValue (e)))
214
215extern /*@exposed@*/ multiVal exprNode_getValue (exprNode p_e) /*@*/ ;
a0a162cd 216extern long exprNode_getLongValue (exprNode p_e) /*@*/ ;
885824d3 217
218extern /*@observer@*/ cstring exprNode_unparseFirst (exprNode p_e) /*@*/ ;
909cf5eb 219extern void exprNode_revealState (exprNode p_e) /*@modifies g_messagestream@*/ ;
220
885824d3 221extern /*@observer@*/ guardSet exprNode_getForGuards (exprNode p_pred) /*@*/ ;
3e3ec469 222extern bool exprNode_loopMustExec (exprNode p_forPred) /*@*/ ;
223
885824d3 224extern bool exprNode_isNullValue (exprNode p_e) /*@*/ ;
225extern /*@exposed@*/ sRef exprNode_getSref (exprNode p_e) /*@*/ ;
e83c79ec 226extern /*@exposed@*/ uentry exprNode_getUentry (exprNode p_e)
885824d3 227 /*@globals internalState@*/ ;
228extern void exprNode_produceGuards (exprNode p_pred) /*@modifies p_pred@*/ ;
6970c11b 229
885824d3 230extern /*@observer@*/ fileloc exprNode_loc (exprNode p_e) /*@*/ ;
6970c11b 231extern /*@observer@*/ fileloc exprNode_getLoc (exprNode p_e) /*@*/ ;
232# define exprNode_getLoc exprNode_loc
233
885824d3 234extern exprNode
235 exprNode_charLiteral (char p_c, cstring p_text, /*@only@*/ fileloc p_loc) /*@*/ ;
236extern /*@observer@*/ exprNode exprNode_makeMustExit (void) /*@*/ ;
237extern exprNode
238 exprNode_cond (/*@keep@*/ exprNode p_pred, /*@keep@*/ exprNode p_ifclause,
239 /*@keep@*/ exprNode p_elseclause) /*@*/ ;
368f75ae 240
241extern exprNode
242exprNode_condIfOmit (/*@keep@*/ exprNode p_pred,
243 /*@keep@*/ exprNode p_elseclause) /*@*/ ;
244
885824d3 245extern exprNode exprNode_makeError(void) /*@*/ ;
246
247extern exprNode exprNode_makeInitBlock (lltok p_brace, /*@only@*/ exprNodeList p_inits) /*@*/ ;
248
249extern exprNode exprNode_functionCall (/*@only@*/ exprNode p_f,
250 /*@only@*/ exprNodeList p_args) /*@*/ ;
251extern /*@notnull@*/ exprNode
252 exprNode_fromIdentifier (/*@observer@*/ uentry p_c) /*@globals internalState@*/ ;
253extern exprNode exprNode_fromUIO (cstring p_c) /*@globals internalState@*/ ;
28bf4b0b 254extern exprNode exprNode_fieldAccess (/*@only@*/ exprNode p_s,
255 /*@only@*/ lltok p_dot,
256 /*@only@*/ cstring p_f) /*@*/ ;
257
258extern exprNode exprNode_arrowAccess (/*@only@*/ exprNode p_s,
259 /*@only@*/ lltok p_arrow,
260 /*@only@*/ cstring p_f) /*@*/ ;
261
885824d3 262extern exprNode exprNode_postOp (/*@only@*/ exprNode p_e, /*@only@*/ lltok p_op)
263 /*@modifies p_e@*/ ;
264extern exprNode exprNode_preOp (/*@only@*/ exprNode p_e, /*@only@*/ lltok p_op) /*@*/ ;
265extern exprNode exprNode_addParens (/*@only@*/ lltok p_lpar, /*@only@*/ exprNode p_e) /*@*/ ;
266extern exprNode exprNode_offsetof (/*@only@*/ qtype p_qt, /*@only@*/ cstringList p_s) /*@*/ ;
267extern exprNode exprNode_sizeofType (/*@only@*/ qtype p_qt) /*@*/ ;
268extern exprNode exprNode_sizeofExpr (/*@only@*/ exprNode p_e) /*@*/ ;
269extern exprNode exprNode_alignofType (/*@only@*/ qtype p_qt) /*@*/ ;
270extern exprNode exprNode_alignofExpr (/*@only@*/ exprNode p_e) /*@*/ ;
271extern exprNode
272 exprNode_op (/*@only@*/ exprNode p_e1, /*@keep@*/ exprNode p_e2, /*@only@*/ lltok p_op) /*@*/ ;
273extern exprNode
274 exprNode_assign (/*@only@*/ exprNode p_e1, /*@only@*/ exprNode p_e2, /*@only@*/ lltok p_op) ;
275extern exprNode
276 exprNode_arrayFetch (/*@only@*/ exprNode p_e1, /*@only@*/ exprNode p_e2)
277 /*@modifies p_e1, p_e2@*/ ;
278
279extern void exprNode_free (/*@only@*/ exprNode p_e) ;
280extern exprNode
281 exprNode_vaArg (/*@only@*/ lltok p_tok, /*@only@*/ exprNode p_arg, /*@only@*/ qtype p_qt)
282 /*@globals internalState@*/ ;
283
abd7f895 284extern bool exprNode_isMultiStatement (exprNode p_e) /*@*/ ;
285
28bf4b0b 286/*
287** Has surrounding quotes.
288*/
289
abd7f895 290extern /*@only@*/ /*@notnull@*/ exprNode
885824d3 291 exprNode_stringLiteral (/*@only@*/ cstring p_t, /*@only@*/ fileloc p_loc) /*@*/ ;
28bf4b0b 292
abd7f895 293extern /*@only@*/ /*@notnull@*/ exprNode
e0b363ad 294 exprNode_wideStringLiteral (/*@only@*/ cstring p_t, /*@only@*/ fileloc p_loc) /*@*/ ;
295
28bf4b0b 296/*
297** No surrounding quotes.
298*/
299
abd7f895 300extern /*@notnull@*/ exprNode
28bf4b0b 301 exprNode_rawStringLiteral (/*@only@*/ cstring p_t, /*@only@*/ fileloc p_loc) /*@*/ ;
302
885824d3 303extern exprNode exprNode_comma (/*@only@*/ exprNode p_e1, /*@only@*/ exprNode p_e2) /*@*/ ;
304extern exprNode exprNode_labelMarker (/*@only@*/ cstring p_label);
305extern exprNode
306 exprNode_notReached (/*@returned@*/ exprNode p_stmt);
307
308extern
309exprNode exprNode_caseMarker (/*@only@*/ exprNode p_test, bool p_fallThrough) /*@*/ ;
310
311extern exprNode exprNode_concat (/*@only@*/ exprNode p_e1, /*@only@*/ exprNode p_e2);
abd7f895 312extern /*@notnull@*/ exprNode exprNode_createTok (/*@only@*/ lltok p_t) /*@*/ ;
4cccc6ad 313extern exprNode exprNode_statement (/*@only@*/ exprNode p_e, /*@only@*/ lltok p_t);
885824d3 314extern exprNode exprNode_makeBlock (/*@only@*/ exprNode p_e);
abd7f895 315extern exprNode exprNode_compoundStatementExpression (/*@only@*/ lltok p_tlparen, /*@only@*/ exprNode p_e) ;
2e127cb8 316
80489f0a 317extern void exprNode_checkIfPred (exprNode p_pred) /*@modifies g_warningstream@*/ ;
2e127cb8 318
885824d3 319extern exprNode exprNode_if (/*@only@*/ exprNode p_pred, /*@only@*/ exprNode p_tclause);
320extern exprNode
321 exprNode_ifelse (/*@only@*/ exprNode p_pred, /*@only@*/ exprNode p_tclause,
322 /*@only@*/ exprNode p_eclause);
323extern exprNode exprNode_switch (/*@only@*/ exprNode p_e, /*@only@*/ exprNode p_s);
324extern exprNode exprNode_while (/*@keep@*/ exprNode p_t, /*@keep@*/ exprNode p_b);
325extern exprNode exprNode_doWhile (/*@only@*/ exprNode p_b, /*@only@*/ exprNode p_t);
326extern /*@notnull@*/ /*@only@*/ exprNode exprNode_goto (/*@only@*/ cstring p_label);
327extern exprNode exprNode_continue (/*@only@*/ lltok p_l, int p_qcontinue);
328extern exprNode exprNode_break (/*@only@*/ lltok p_l, int p_bqual);
329extern exprNode exprNode_nullReturn (/*@only@*/ lltok p_t);
330extern exprNode exprNode_return (/*@only@*/ exprNode p_e);
331extern /*@dependent@*/ /*@observer@*/ cstring
28bf4b0b 332exprNode_unparse (/*@temp@*/ exprNode p_e) /*@*/ ;
885824d3 333
abd7f895 334extern /*@falsewhennull@*/ bool exprNode_isBlock (exprNode p_e) /*@*/ ;
e5081f8c 335extern /*@falsewhennull@*/ bool exprNode_isCharLiteral (exprNode p_e) /*@*/ ;
336extern /*@falsewhennull@*/ bool exprNode_isNumLiteral (exprNode p_e) /*@*/ ;
885824d3 337
338extern exprNode
339 exprNode_makeInitialization (/*@only@*/ idDecl p_t, /*@only@*/ exprNode p_e);
28bf4b0b 340
341exprNode exprNode_makeEmptyInitialization (/*@only@*/ idDecl p_t) ;
342
343extern bool exprNode_isInitializer (exprNode p_e) /*@*/ ;
344
885824d3 345extern bool exprNode_matchType (ctype p_expected, exprNode p_e);
346
347extern /*@notnull@*/ /*@only@*/ exprNode
348 exprNode_defaultMarker (/*@only@*/ lltok p_def, bool p_fallThrough);
349
350extern exprNode
351 exprNode_iter (/*@observer@*/ uentry p_name, /*@only@*/ exprNodeList p_alist,
352 /*@only@*/ exprNode p_body, /*@observer@*/ uentry p_end);
353extern exprNode exprNode_iterId (/*@observer@*/ uentry p_c);
354extern exprNode exprNode_iterExpr (/*@returned@*/ exprNode p_e);
355extern exprNode exprNode_iterNewId (/*@only@*/ cstring p_s);
356extern exprNode
357 exprNode_iterStart (/*@observer@*/ uentry p_name, /*@only@*/ exprNodeList p_alist);
6fcd0b1e 358extern exprNode exprNode_numLiteral (ctype p_c, /*@temp@*/ cstring p_t,
359 /*@only@*/ fileloc p_loc, long p_val) /*@*/ ;
885824d3 360extern void exprNode_initMod (void) /*@modifies internalState@*/ ;
361extern exprNode exprNode_for (/*@keep@*/ exprNode p_inc, /*@keep@*/ exprNode p_body);
362extern exprNode
363 exprNode_forPred (/*@only@*/ exprNode p_init,
364 /*@only@*/ exprNode p_test, /*@only@*/ exprNode p_inc);
6fcd0b1e 365extern exprNode exprNode_floatLiteral (double p_d, ctype p_ct,
366 cstring p_text, /*@only@*/ fileloc p_loc) /*@*/ ;
885824d3 367extern /*@notnull@*/ exprNode exprNode_createId (/*@observer@*/ uentry p_c);
5c2f3045 368extern /*@notnull@*/ exprNode exprNode_makeConstantString (/*@temp@*/ cstring p_c, /*@only@*/ fileloc p_loc) /*@*/ ;
885824d3 369extern exprNode exprNode_cast (/*@only@*/ lltok p_tok, /*@only@*/ exprNode p_e, /*@only@*/ qtype p_q);
370extern bool exprNode_matchLiteral (ctype p_expected, exprNode p_e);
371extern void exprNode_checkUseParam (exprNode p_current);
28bf4b0b 372extern void exprNode_checkSet (exprNode p_e, /*@exposed@*/ sRef p_s);
373extern void exprNode_checkMSet (exprNode p_e, /*@exposed@*/ sRef p_s);
885824d3 374extern exprNode exprNode_checkExpr (/*@returned@*/ exprNode p_e);
375extern bool exprNode_mustEscape (exprNode p_e);
376extern bool exprNode_errorEscape (exprNode p_e);
377extern bool exprNode_mayEscape (exprNode p_e);
378extern exprNode exprNode_whilePred (/*@only@*/ exprNode p_test);
379extern exprNode
380 exprNode_updateLocation (/*@returned@*/ exprNode p_e, /*@temp@*/ fileloc p_loc);
381extern void exprNode_freeShallow (/*@only@*/ exprNode p_e);
382extern void exprNode_destroyMod (void) /*@modifies internalState@*/ ;
abd7f895 383extern /*@falsewhennull@*/ bool exprNode_isAssign (exprNode p_e) /*@*/ ;
885824d3 384
385/*@-exportlocal@*/
386extern bool exprNode_isDefaultMarker (exprNode p_e) /*@*/ ;
387extern bool exprNode_isCaseMarker (exprNode p_e) /*@*/ ;
388extern bool exprNode_isLabelMarker (exprNode p_e) /*@*/ ;
389/*@=exportlocal@*/
390
28bf4b0b 391extern /*@only@*/ exprNode exprNode_combineLiterals (/*@only@*/ exprNode p_e, /*@only@*/ exprNode p_rest) ;
392
393extern /*@only@*/ fileloc exprNode_getNextSequencePoint (exprNode p_e) ;
4cccc6ad 394
103db890 395/*drl 01-20-2001*/
28bf4b0b 396exprNode exprNode_createNew(ctype p_c);
397
d30bc0c7 398/* drl 07-25-01 */
d30bc0c7 399bool exprNode_isInitBlock (exprNode p_e);
400
885824d3 401# else
402# error "Multiple include"
403# endif
git-cvsimport mirror of splint
This page took 0.125475 seconds and 5 git commands to generate.