/*
** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2002 University of Virginia,
+** Copyright (C) 1994-2003 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
# include "splintMacros.nf"
# include "basic.h"
-static /*@only@*/ /*@notnull@*/ /*@special@*/ functionClause /*@i32 need special? @*/
+static /*@only@*/ /*@notnull@*/ /*@special@*/ functionClause
functionClause_alloc (functionClauseKind kind) /*@defines result->kind@*/
{
functionClause res = (functionClause) dmalloc (sizeof (*res));
}
extern functionClause functionClause_createState (stateClause node) /*@*/
-{
- functionClause res = functionClause_alloc (FCK_STATE);
- res->val.state = node;
- return res;
+{
+ if (stateClause_hasEmptyReferences (node) &&
+ (!stateClause_isMetaState (node) ) )
+ {
+ DPRINTF((message("functionClause_createState:: Returning functionClause_undefined" ) ));
+ stateClause_free (node);
+ return functionClause_undefined;
+ }
+ else
+ {
+ functionClause res = functionClause_alloc (FCK_STATE);
+ res->val.state = node;
+ return res;
+ }
}
extern functionClause functionClause_createEnsures (functionConstraint node) /*@*/