/*
-** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
+** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
** See ../LICENSE for license information.
**
*/
XPR_INIT, XPR_FACCESS, XPR_ARROW, XPR_CONST, XPR_STRINGLITERAL,
XPR_NUMLIT, XPR_BODY, XPR_NODE, XPR_ITERCALL, XPR_TOK,
XPR_WHILEPRED, XPR_CASE, XPR_FTCASE, XPR_DEFAULT, XPR_FTDEFAULT,
- XPR_BLOCK, XPR_INITBLOCK, XPR_LABEL
+ XPR_BLOCK, XPR_INITBLOCK,
+ XPR_LABEL
} exprKind;
-typedef struct _exprOffsetof
+typedef struct
{
/*@only@*/ qtype q;
/*@only@*/ cstringList field;
} *exprOffsetof;
-typedef struct _exprPair
+typedef struct
{
/*@only@*/ exprNode a;
/*@only@*/ exprNode b;
} *exprPair;
-typedef struct _exprTriple
+typedef struct
{
/*@only@*/ exprNode pred;
/*@only@*/ exprNode tbranch;
/*@only@*/ exprNode fbranch;
} *exprTriple;
-typedef struct _exprIter
+typedef struct
{
/*@dependent@*/ /*@observer@*/ uentry sname;
/*@only@*/ exprNodeList args;
/*@dependent@*/ /*@observer@*/ uentry ename;
} *exprIter;
-typedef struct _exprCall
+typedef struct
{
/*@only@*/ exprNode fcn;
/*@only@*/ exprNodeList args;
} *exprCall;
-typedef struct _exprIterCall
+typedef struct
{
/*@dependent@*/ /*@exposed@*/ uentry iter;
/*@only@*/ exprNodeList args;
} *exprIterCall;
-typedef struct _exprOp
+typedef struct
{
/*@only@*/ exprNode a;
/*@only@*/ exprNode b;
lltok op;
} *exprOp;
-typedef struct _exprField
+typedef struct
{
/*@only@*/ exprNode rec;
/*@only@*/ cstring field;
} *exprField;
-typedef struct _exprUop
+typedef struct
{
/*@only@*/ exprNode a;
lltok op;
} *exprUop;
-typedef struct _exprCast
+typedef struct
{
/*@only@*/ exprNode exp;
lltok tok;
qtype q;
} *exprCast;
-typedef struct _exprInit
+typedef struct
{
/*@only@*/ exprNode exp;
idDecl id;
} *exprInit;
-typedef /*@null@*/ union _exprData
+typedef /*@null@*/ union
{
cstring literal;
cstring id;
- lltok *tok;
+ lltok tok;
qtype qt; /* sizeof(type) */
/* use for any 2-operator (comma, arrayFetch, case, stmt) */
exprPair pair;
/*@constant null exprData exprData_undefined; @*/
# define exprData_undefined ((exprData) NULL)
-struct _exprNode
+struct s_exprNode
{
bool isJumpPoint BOOLBITS; /* expr can be reached non-sequentially */
bool canBreak BOOLBITS; /* expr can break (has break, continue) */
fileloc loc;
/*@relnull@*/ exprData edata;
cstring etext;
- environmentTable environment;
- constraintList requiresConstraints;
- constraintList ensuresConstraints;
- //these two are used only for boolean expressions
- //they store the ensures constraints for the true and false cases
- constraintList trueEnsuresConstraints;
- constraintList falseEnsuresConstraints;
+ /*@notnull@*/ constraintList requiresConstraints;
+ /*@notnull@*/ constraintList ensuresConstraints;
+
+ /*
+ ** These two are used only for boolean expressions,
+ ** they store the ensures constraints for the true and false cases
+ */
+
+ /*@notnull@*/ constraintList trueEnsuresConstraints;
+ /*@notnull@*/ constraintList falseEnsuresConstraints;
} ;
/*@constant null exprNode exprNode_undefined; @*/
# define exprNode_undefined ((exprNode)NULL)
-extern /*@falsenull@*/ bool exprNode_isDefined (exprNode p_e) /*@*/ ;
-extern /*@unused@*/ /*@truenull@*/ bool exprNode_isUndefined (exprNode p_e) /*@*/ ;
-extern /*@truenull@*/ bool exprNode_isError (exprNode p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool exprNode_isDefined (exprNode p_e) /*@*/ ;
+extern /*@unused@*/ /*@nullwhentrue@*/ bool exprNode_isUndefined (exprNode p_e) /*@*/ ;
+extern /*@nullwhentrue@*/ bool exprNode_isError (exprNode p_e) /*@*/ ;
# define exprNode_isDefined(e) ((e) != exprNode_undefined)
# define exprNode_isUndefined(e) ((e) == exprNode_undefined)
# define exprNode_getType(e) \
(exprNode_isDefined(e) ? (e)->typ : ctype_unknown)
-extern /*@unused@*/ /*@falsenull@*/ bool exprNode_isInParens (/*@sef@*/ exprNode p_e) /*@*/ ;
+extern /*@unused@*/ /*@falsewhennull@*/ bool exprNode_isInParens (/*@sef@*/ exprNode p_e) /*@*/ ;
# define exprNode_isInParens(e) \
(exprNode_isDefined(e) && (e)->kind == XPR_PARENS)
-extern bool exprNode_isStringLiteral (/*@sef@*/ exprNode p_e);
+extern bool exprNode_isStringLiteral (/*@sef@*/ exprNode p_e) /*@*/ ;
# define exprNode_isStringLiteral(e) \
(exprNode_isDefined(e) && (e)->kind == XPR_STRINGLITERAL)
extern /*@observer@*/ cstring exprNode_unparseFirst (exprNode p_e) /*@*/ ;
extern /*@observer@*/ guardSet exprNode_getForGuards (exprNode p_pred) /*@*/ ;
+extern bool exprNode_loopMustExec (exprNode p_forPred) /*@*/ ;
+
extern bool exprNode_isNullValue (exprNode p_e) /*@*/ ;
extern /*@exposed@*/ sRef exprNode_getSref (exprNode p_e) /*@*/ ;
-extern /*@observer@*/ uentry exprNode_getUentry (exprNode p_e)
+extern /*@exposed@*/ uentry exprNode_getUentry (exprNode p_e)
/*@globals internalState@*/ ;
extern void exprNode_produceGuards (exprNode p_pred) /*@modifies p_pred@*/ ;
+
extern /*@observer@*/ fileloc exprNode_loc (exprNode p_e) /*@*/ ;
+extern /*@observer@*/ fileloc exprNode_getLoc (exprNode p_e) /*@*/ ;
+# define exprNode_getLoc exprNode_loc
+
extern exprNode
exprNode_charLiteral (char p_c, cstring p_text, /*@only@*/ fileloc p_loc) /*@*/ ;
extern /*@observer@*/ exprNode exprNode_makeMustExit (void) /*@*/ ;
extern /*@notnull@*/ exprNode
exprNode_fromIdentifier (/*@observer@*/ uentry p_c) /*@globals internalState@*/ ;
extern exprNode exprNode_fromUIO (cstring p_c) /*@globals internalState@*/ ;
-extern exprNode exprNode_fieldAccess (/*@only@*/ exprNode p_s, /*@only@*/ cstring p_f) /*@*/ ;
-extern exprNode exprNode_arrowAccess (/*@only@*/ exprNode p_s, /*@only@*/ cstring p_f) /*@*/ ;
+extern exprNode exprNode_fieldAccess (/*@only@*/ exprNode p_s,
+ /*@only@*/ lltok p_dot,
+ /*@only@*/ cstring p_f) /*@*/ ;
+
+extern exprNode exprNode_arrowAccess (/*@only@*/ exprNode p_s,
+ /*@only@*/ lltok p_arrow,
+ /*@only@*/ cstring p_f) /*@*/ ;
+
extern exprNode exprNode_postOp (/*@only@*/ exprNode p_e, /*@only@*/ lltok p_op)
/*@modifies p_e@*/ ;
extern exprNode exprNode_preOp (/*@only@*/ exprNode p_e, /*@only@*/ lltok p_op) /*@*/ ;
exprNode_vaArg (/*@only@*/ lltok p_tok, /*@only@*/ exprNode p_arg, /*@only@*/ qtype p_qt)
/*@globals internalState@*/ ;
-extern exprNode
+extern bool exprNode_isMultiStatement (exprNode p_e) /*@*/ ;
+
+/*
+** Has surrounding quotes.
+*/
+
+extern /*@only@*/ /*@notnull@*/ exprNode
exprNode_stringLiteral (/*@only@*/ cstring p_t, /*@only@*/ fileloc p_loc) /*@*/ ;
+
+extern /*@only@*/ /*@notnull@*/ exprNode
+ exprNode_wideStringLiteral (/*@only@*/ cstring p_t, /*@only@*/ fileloc p_loc) /*@*/ ;
+
+/*
+** No surrounding quotes.
+*/
+
+extern /*@notnull@*/ exprNode
+ exprNode_rawStringLiteral (/*@only@*/ cstring p_t, /*@only@*/ fileloc p_loc) /*@*/ ;
+
extern exprNode exprNode_comma (/*@only@*/ exprNode p_e1, /*@only@*/ exprNode p_e2) /*@*/ ;
extern exprNode exprNode_labelMarker (/*@only@*/ cstring p_label);
extern exprNode
exprNode exprNode_caseMarker (/*@only@*/ exprNode p_test, bool p_fallThrough) /*@*/ ;
extern exprNode exprNode_concat (/*@only@*/ exprNode p_e1, /*@only@*/ exprNode p_e2);
-extern exprNode exprNode_createTok (/*@only@*/ lltok p_t) /*@*/ ;
+extern /*@notnull@*/ exprNode exprNode_createTok (/*@only@*/ lltok p_t) /*@*/ ;
extern exprNode exprNode_statement (/*@only@*/ exprNode p_e, /*@only@*/ lltok p_t);
extern exprNode exprNode_makeBlock (/*@only@*/ exprNode p_e);
+extern exprNode exprNode_compoundStatementExpression (/*@only@*/ lltok p_tlparen, /*@only@*/ exprNode p_e) ;
+
+extern void exprNode_checkIfPred (exprNode p_pred) /*@modifies g_warningstream@*/ ;
+
extern exprNode exprNode_if (/*@only@*/ exprNode p_pred, /*@only@*/ exprNode p_tclause);
extern exprNode
exprNode_ifelse (/*@only@*/ exprNode p_pred, /*@only@*/ exprNode p_tclause,
extern exprNode exprNode_nullReturn (/*@only@*/ lltok p_t);
extern exprNode exprNode_return (/*@only@*/ exprNode p_e);
extern /*@dependent@*/ /*@observer@*/ cstring
- exprNode_unparse (exprNode p_e) /*@*/ ;
+exprNode_unparse (/*@temp@*/ exprNode p_e) /*@*/ ;
-extern bool exprNode_isCharLit (exprNode p_e) /*@*/ ;
-extern bool exprNode_isNumLit (exprNode p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool exprNode_isBlock (exprNode p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool exprNode_isCharLiteral (exprNode p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool exprNode_isNumLiteral (exprNode p_e) /*@*/ ;
extern exprNode
exprNode_makeInitialization (/*@only@*/ idDecl p_t, /*@only@*/ exprNode p_e);
+
+exprNode exprNode_makeEmptyInitialization (/*@only@*/ idDecl p_t) ;
+
+extern bool exprNode_isInitializer (exprNode p_e) /*@*/ ;
+
extern bool exprNode_matchType (ctype p_expected, exprNode p_e);
extern /*@notnull@*/ /*@only@*/ exprNode
extern exprNode exprNode_iterNewId (/*@only@*/ cstring p_s);
extern exprNode
exprNode_iterStart (/*@observer@*/ uentry p_name, /*@only@*/ exprNodeList p_alist);
-extern exprNode
- exprNode_numLiteral (ctype p_c, /*@temp@*/ cstring p_t,
- /*@only@*/ fileloc p_loc, long p_val);
+extern exprNode exprNode_numLiteral (ctype p_c, /*@temp@*/ cstring p_t,
+ /*@only@*/ fileloc p_loc, long p_val) /*@*/ ;
extern void exprNode_initMod (void) /*@modifies internalState@*/ ;
extern exprNode exprNode_for (/*@keep@*/ exprNode p_inc, /*@keep@*/ exprNode p_body);
extern exprNode
exprNode_forPred (/*@only@*/ exprNode p_init,
/*@only@*/ exprNode p_test, /*@only@*/ exprNode p_inc);
-extern exprNode
- exprNode_floatLiteral (double p_d, ctype p_ct,
- cstring p_text, /*@only@*/ fileloc p_loc);
+extern exprNode exprNode_floatLiteral (double p_d, ctype p_ct,
+ cstring p_text, /*@only@*/ fileloc p_loc) /*@*/ ;
extern /*@notnull@*/ exprNode exprNode_createId (/*@observer@*/ uentry p_c);
+extern /*@notnull@*/ exprNode exprNode_makeConstantString (/*@temp@*/ cstring p_c, /*@only@*/ fileloc p_loc) /*@*/ ;
extern exprNode exprNode_cast (/*@only@*/ lltok p_tok, /*@only@*/ exprNode p_e, /*@only@*/ qtype p_q);
extern bool exprNode_matchLiteral (ctype p_expected, exprNode p_e);
extern void exprNode_checkUseParam (exprNode p_current);
-extern void exprNode_checkSet (exprNode p_e, sRef p_s);
-extern void exprNode_checkMSet (exprNode p_e, sRef p_s);
+extern void exprNode_checkSet (exprNode p_e, /*@exposed@*/ sRef p_s);
+extern void exprNode_checkMSet (exprNode p_e, /*@exposed@*/ sRef p_s);
extern exprNode exprNode_checkExpr (/*@returned@*/ exprNode p_e);
extern bool exprNode_mustEscape (exprNode p_e);
extern bool exprNode_errorEscape (exprNode p_e);
exprNode_updateLocation (/*@returned@*/ exprNode p_e, /*@temp@*/ fileloc p_loc);
extern void exprNode_freeShallow (/*@only@*/ exprNode p_e);
extern void exprNode_destroyMod (void) /*@modifies internalState@*/ ;
-extern bool exprNode_isAssign (exprNode p_e) /*@*/ ;
-
-/* added 8-15-00
- by DRL */
-extern fileloc exprNode_getfileloc (exprNode p_e) ;
+extern /*@falsewhennull@*/ bool exprNode_isAssign (exprNode p_e) /*@*/ ;
/*@-exportlocal@*/
extern bool exprNode_isDefaultMarker (exprNode p_e) /*@*/ ;
extern bool exprNode_isLabelMarker (exprNode p_e) /*@*/ ;
/*@=exportlocal@*/
-/* evs 2000-08-22 */
-fileloc exprNode_getNextSequencePoint (exprNode p_e) /*@*/ ;
-
-/*drl 09-08-2008 */
-exprNode exprNode_fakeCopy (exprNode e);
-# else
-# error "Multiple include"
-# endif
-
-
-
-
-
-
-
-
-
-
-
-
-
+extern /*@only@*/ exprNode exprNode_combineLiterals (/*@only@*/ exprNode p_e, /*@only@*/ exprNode p_rest) ;
+extern /*@only@*/ fileloc exprNode_getNextSequencePoint (exprNode p_e) ;
+/*drl 01-20-2001*/
+exprNode exprNode_createNew(ctype p_c);
+/* drl 07-25-01 */
+bool exprNode_isInitBlock (exprNode p_e);
+# else
+# error "Multiple include"
+# endif
andersk / splint.git / blobdiff