X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/3814599dbdafeaf8cb335d07f1d1bf1729a98417..5b99bfd6792ab9229bb5b1d9048833d21b22ecef:/src/metaStateExpression.c diff --git a/src/metaStateExpression.c b/src/metaStateExpression.c index e3287d1..5d92955 100644 --- a/src/metaStateExpression.c +++ b/src/metaStateExpression.c @@ -1,6 +1,6 @@ /* -** LCLint - annotation-assisted static program checker -** Copyright (C) 1994-2001 University of Virginia, +** Splint - annotation-assisted static program checker +** Copyright (C) 1994-2003 University of Virginia, ** Massachusetts Institute of Technology ** ** This program is free software; you can redistribute it and/or modify it @@ -17,17 +17,16 @@ ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, ** MA 02111-1307, USA. ** -** For information on lclint: lclint-request@cs.virginia.edu -** To report a bug: lclint-bug@cs.virginia.edu -** For more information: http://lclint.cs.virginia.edu +** For information on splint: info@splint.org +** To report a bug: splint-bug@splint.org +** For more information: http://www.splint.org */ /* ** metaStateExpression.c */ -# include "lclintMacros.nf" +# include "splintMacros.nf" # include "basic.h" -# include "mtincludes.h" metaStateExpression metaStateExpression_create (/*@only@*/ metaStateSpecifier spec) @@ -80,6 +79,24 @@ metaStateExpression metaStateExpression_copy (metaStateExpression m) } } +metaStateSpecifier metaStateExpression_getSpecifier (metaStateExpression m) +{ + llassert (m != NULL); + return m->spec; +} + +bool metaStateExpression_isMerge (metaStateExpression m) +{ + return (metaStateExpression_isDefined (m) + && metaStateExpression_isDefined (m->rest)); +} + +/*@observer@*/ metaStateExpression metaStateExpression_getRest (metaStateExpression m) +{ + llassert (m != NULL); + return m->rest; +} + void metaStateExpression_free (/*@only@*/ metaStateExpression m) { llassert (m != NULL); @@ -93,4 +110,3 @@ void metaStateExpression_free (/*@only@*/ metaStateExpression m) sfree (m); } -