---

abstract.c File Reference

#include "lclintMacros.nf"
#include "llbasic.h"
#include "lslparse.h"
#include "llgrammar.h"
#include "lclscan.h"
#include "lh.h"
#include "imports.h"

Go to the source code of this file.

Functions
void	resetImports (cstring current)
void	abstract_init ()
void	declareForwardType (declaratorNode declare)
void	LCLBuiltins (void)
interfaceNodeList	consInterfaceNode ( interfaceNode n, interfaceNodeList ns)
interfaceNode	makeInterfaceNodeImports ( importNodeList x)
interfaceNode	makeInterfaceNodeUses ( traitRefNodeList x)
interfaceNode	interfaceNode_makeConst ( constDeclarationNode x)
interfaceNode	interfaceNode_makeVar ( varDeclarationNode x)
interfaceNode	interfaceNode_makeType ( typeNode x)
interfaceNode	interfaceNode_makeFcn ( fcnNode x)
interfaceNode	interfaceNode_makeClaim ( claimNode x)
interfaceNode	interfaceNode_makeIter ( iterNode x)
interfaceNode	interfaceNode_makePrivConst ( constDeclarationNode x)
interfaceNode	interfaceNode_makePrivVar ( varDeclarationNode x)
interfaceNode	interfaceNode_makePrivType ( typeNode x)
interfaceNode	interfaceNode_makePrivFcn ( fcnNode x)
cstring	exportNode_unparse (exportNode n)
cstring	privateNode_unparse (privateNode n)
bool	ltoken_similar (ltoken t1, ltoken t2)
cstring	iterNode_unparse ( iterNode i)
cstring	fcnNode_unparse ( fcnNode f)
cstring	varDeclarationNode_unparse ( varDeclarationNode x)
cstring	typeNode_unparse ( typeNode t)
cstring	constDeclarationNode_unparse ( constDeclarationNode x)
storeRefNode	makeStoreRefNodeTerm ( termNode t)
storeRefNode	makeStoreRefNodeType ( lclTypeSpecNode t, bool isObj)
storeRefNode	makeStoreRefNodeInternal (void)
storeRefNode	makeStoreRefNodeSystem (void)
modifyNode	makeModifyNodeSpecial ( ltoken t, bool modifiesNothing)
modifyNode	makeModifyNodeRef ( ltoken t, storeRefNodeList y)
ltoken	termNode_errorToken ( termNode n)
ltoken	nameNode_errorToken ( nameNode nn)
ltoken	lclTypeSpecNode_errorToken ( lclTypeSpecNode t)
letDeclNode	makeLetDeclNode (ltoken varid, lclTypeSpecNode t, termNode term)
programNode	makeProgramNodeAction ( programNodeList x, actionKind k)
programNode	makeProgramNode ( stmtNode x)
typeNode	makeAbstractTypeNode ( abstractNode x)
typeNode	makeExposedTypeNode ( exposedNode x)
importNode	importNode_makePlain ( ltoken t)
importNode	importNode_makeBracketed ( ltoken t)
importNode	importNode_makeQuoted ( ltoken t)
void	checkBrackets (ltoken lb, ltoken rb)
traitRefNode	makeTraitRefNode ( ltokenList fl, renamingNode r)
cstring	printLeaves2 (ltokenList f)
cstring	printRawLeaves2 (ltokenList f)
renamingNode	makeRenamingNode ( typeNameNodeList n, replaceNodeList r)
cstring	renamingNode_unparse ( renamingNode x)
replaceNode	makeReplaceNameNode (ltoken t, typeNameNode tn, nameNode nn)
replaceNode	makeReplaceNode (ltoken t, typeNameNode tn, bool is_ctype, ltoken ct, nameNode nn, sigNode sn)
cstring	replaceNode_unparse ( replaceNode x)
nameNode	makeNameNodeForm ( opFormNode opform)
nameNode	makeNameNodeId ( ltoken opid)
cstring	nameNode_unparse ( nameNode n)
sigNode	makesigNode (ltoken t, ltokenList domain, ltoken range)
cstring	sigNode_unparse ( sigNode n)
void	sigNode_markOwned (sigNode n)
cstring	sigNode_unparseText ( sigNode n)
opFormNode	makeOpFormNode (ltoken t, opFormKind k, opFormUnion u, ltoken close)
cstring	opFormNode_unparse ( opFormNode n)
typeNameNode	makeTypeNameNode (bool isObj, lclTypeSpecNode t, abstDeclaratorNode n)
typeNameNode	makeTypeNameNodeOp (opFormNode n)
cstring	typeNameNode_unparse ( typeNameNode n)
lclTypeSpecNode	makeLclTypeSpecNodeConj ( lclTypeSpecNode a, lclTypeSpecNode b)
lclTypeSpecNode	makeLclTypeSpecNodeType ( CTypesNode x)
lclTypeSpecNode	makeLclTypeSpecNodeSU ( strOrUnionNode x)
lclTypeSpecNode	makeLclTypeSpecNodeEnum ( enumSpecNode x)
lclTypeSpecNode	lclTypeSpecNode_addQual (lclTypeSpecNode n, qual q)
cstring	lclTypeSpecNode_unparse ( lclTypeSpecNode n)
enumSpecNode	makeEnumSpecNode (ltoken t, ltoken optTagId, ltokenList enums)
enumSpecNode	makeEnumSpecNode2 (ltoken t, ltoken tagid)
cstring	enumSpecNode_unparse ( enumSpecNode n)
strOrUnionNode	makestrOrUnionNode (ltoken str, suKind k, ltoken opttagid, stDeclNodeList x)
strOrUnionNode	makeForwardstrOrUnionNode (ltoken str, suKind k, ltoken tagid)
cstring	strOrUnionNode_unparse ( strOrUnionNode n)
stDeclNode	makestDeclNode (lclTypeSpecNode s, declaratorNodeList x)
typeExpr	makeFunctionNode (typeExpr x, paramNodeList p)
typeExpr	makeTypeExpr (ltoken t)
declaratorNode	makeDeclaratorNode (typeExpr t)
cstring	declaratorNode_unparse (declaratorNode x)
declaratorNode	declaratorNode_copy (declaratorNode x)
void	typeExpr_free ( typeExpr x)
cstring	declaratorNode_unparseCode (declaratorNode x)
cstring	typeExpr_unparse ( typeExpr x)
cstring	typeExpr_unparseNoBase ( typeExpr x)
cstring	typeExpr_name ( typeExpr x)
typeExpr	makePointerNode (ltoken star, typeExpr x)
typeExpr	makeArrayNode ( typeExpr x, arrayQualNode a)
constDeclarationNode	makeConstDeclarationNode (lclTypeSpecNode t, initDeclNodeList decls)
varDeclarationNode	makeInternalStateNode (void)
varDeclarationNode	makeFileSystemNode (void)
varDeclarationNode	makeVarDeclarationNode (lclTypeSpecNode t, initDeclNodeList x, bool isGlobal, bool isPrivate)
initDeclNode	makeInitDeclNode (declaratorNode d, termNode x)
abstractNode	makeAbstractNode (ltoken t, ltoken name, bool isMutable, bool isRefCounted, abstBodyNode a)
cstring	abstractNode_unparse (abstractNode n)
void	setExposedType (lclTypeSpecNode s)
exposedNode	makeExposedNode (ltoken t, lclTypeSpecNode s, declaratorInvNodeList d)
cstring	exposedNode_unparse (exposedNode n)
declaratorInvNode	makeDeclaratorInvNode (declaratorNode d, abstBodyNode b)
cstring	declaratorInvNode_unparse (declaratorInvNode d)
cstring	abstBodyNode_unparse (abstBodyNode n)
cstring	abstBodyNode_unparseExposed (abstBodyNode n)
cstring	taggedUnionNode_unparse (taggedUnionNode n)
fcnNode	fcnNode_fromDeclarator ( lclTypeSpecNode t, declaratorNode d)
iterNode	makeIterNode (ltoken id, paramNodeList p)
fcnNode	makeFcnNode (qual specQual, lclTypeSpecNode t, declaratorNode d, globalList g, varDeclarationNodeList privateinits, letDeclNodeList lets, lclPredicateNode checks, lclPredicateNode requires, modifyNode m, lclPredicateNode ensures, lclPredicateNode claims)
claimNode	makeClaimNode (ltoken id, paramNodeList p, globalList g, letDeclNodeList lets, lclPredicateNode requires, programNode b, lclPredicateNode ensures)
lclPredicateNode	makeIntraClaimNode (ltoken t, lclPredicateNode n)
lclPredicateNode	makeRequiresNode (ltoken t, lclPredicateNode n)
lclPredicateNode	makeChecksNode (ltoken t, lclPredicateNode n)
lclPredicateNode	makeEnsuresNode (ltoken t, lclPredicateNode n)
lclPredicateNode	makeLclPredicateNode (ltoken t, termNode n, lclPredicateKind k)
quantifierNode	makeQuantifierNode (varNodeList v, ltoken quant)
arrayQualNode	makeArrayQualNode (ltoken t, termNode term)
varNode	makeVarNode ( ltoken varid, bool isObj, lclTypeSpecNode t)
abstBodyNode	makeAbstBodyNode (ltoken t, fcnNodeList f)
abstBodyNode	makeExposedBodyNode (ltoken t, lclPredicateNode inv)
abstBodyNode	makeAbstBodyNode2 (ltoken t, ltokenList ops)
stmtNode	makeStmtNode (ltoken varId, ltoken fcnId, termNodeList v)
paramNode	makeParamNode (lclTypeSpecNode t, typeExpr d)
paramNode	paramNode_elipsis (void)
cstring	paramNode_unparse (paramNode x)
cstring	lclTypeSpecNode_unparseComments ( lclTypeSpecNode typespec)
cstring	paramNode_unparseComments (paramNode x)
termNode	makeIfTermNode (ltoken ift, termNode ifn, ltoken thent, termNode thenn, ltoken elset, termNode elsen)
termNode	makeInfixTermNode (termNode x, ltoken op, termNode y)
termNode	makeQuantifiedTermNode (quantifierNodeList qn, ltoken open, termNode t, ltoken close)
termNode	makePostfixTermNode ( termNode secondary, ltokenList postfixops)
termNode	makePostfixTermNode2 ( termNode secondary, ltoken postfixop)
termNode	makePrefixTermNode (ltoken op, termNode arg)
termNode	makeOpCallTermNode (ltoken op, ltoken open, termNodeList args, ltoken close)
termNode	CollapseInfixTermNode ( termNode secondary, termNodeList infix)
termNodeList	pushInfixOpPartNode ( termNodeList x, ltoken op, termNode secondary)
termNode	updateMatchedNode ( termNode left, termNode t, termNode right)
termNode	updateSqBracketedNode ( termNode left, termNode t, termNode right)
termNode	makeSqBracketedNode (ltoken lbracket, termNodeList args, ltoken rbracket)
termNode	makeMatchedNode (ltoken open, termNodeList args, ltoken close)
termNode	makeSimpleTermNode (ltoken varid)
termNode	makeSelectTermNode (termNode pri, ltoken select, ltoken id)
termNode	makeMapTermNode (termNode pri, ltoken map, ltoken id)
termNode	makeLiteralTermNode (ltoken tok, sort s)
termNode	makeUnchangedTermNode1 (ltoken op, ltoken all)
termNode	makeUnchangedTermNode2 (ltoken op, storeRefNodeList x)
termNode	makeSizeofTermNode (ltoken op, lclTypeSpecNode type)
cstring	claimNode_unparse (claimNode c)
cstring	termNode_unparse ( termNode n)
cstring	modifyNode_unparse ( modifyNode m)
cstring	programNode_unparse (programNode p)
cstring	stmtNode_unparse (stmtNode x)
lslOp	makelslOpNode ( nameNode name, sigNode s)
cstring	lslOp_unparse (lslOp x)
bool	sameNameNode ( nameNode n1, nameNode n2)
CTypesNode	makeCTypesNode ( CTypesNode ctypes, ltoken ct)
CTypesNode	makeTypeSpecifier (ltoken typedefname)
bool	sigNode_equal (sigNode n1, sigNode n2)
sort	typeExpr2ptrSort (sort base, typeExpr t)
sort	lclTypeSpecNode2sort (lclTypeSpecNode type)
lsymbol	checkAndEnterTag (tagKind k, ltoken opttagid)
void	signNode_free ( signNode sn)
cstring	signNode_unparse (signNode sn)
void	enteringFcnScope (lclTypeSpecNode t, declaratorNode d, globalList g)
void	enteringClaimScope (paramNodeList params, globalList g)
sort	sigNode_rangeSort (sigNode sig)
sortList	sigNode_domain (sigNode sig)
opFormUnion	opFormUnion_createAnyOp ( ltoken t)
opFormUnion	opFormUnion_createMiddle (int middle)
paramNode	markYieldParamNode (paramNode p)
lclTypeSpecNode	lclTypeSpecNode_copy ( lclTypeSpecNode n)
void	nameNode_free (nameNode n)
bool	lslOp_equal (lslOp x, lslOp y)
void	lslOp_free (lslOp x)
void	sigNode_free (sigNode x)
void	declaratorNode_free ( declaratorNode x)
void	fcnNode_free ( fcnNode f)
void	declaratorInvNode_free ( declaratorInvNode x)
lslOp	lslOp_copy (lslOp x)
sigNode	sigNode_copy (sigNode s)
nameNode	nameNode_copy ( nameNode n)
nameNode	nameNode_copySafe (nameNode n)
bool	initDeclNode_isRedeclaration (initDeclNode d)
void	termNode_free ( termNode t)
termNode	termNode_copySafe (termNode t)
void	importNode_free ( importNode x)
void	initDeclNode_free ( initDeclNode x)
void	letDeclNode_free ( letDeclNode x)
void	pairNode_free ( pairNode x)
paramNode	paramNode_copy ( paramNode p)
void	paramNode_free ( paramNode x)
void	programNode_free ( programNode x)
quantifierNode	quantifierNode_copy (quantifierNode x)
void	quantifierNode_free ( quantifierNode x)
void	replaceNode_free ( replaceNode x)
storeRefNode	storeRefNode_copy (storeRefNode x)
void	storeRefNode_free ( storeRefNode x)
stDeclNode	stDeclNode_copy (stDeclNode x)
void	stDeclNode_free ( stDeclNode x)
void	traitRefNode_free ( traitRefNode x)
void	typeNameNode_free ( typeNameNode n)
void	varDeclarationNode_free ( varDeclarationNode x)
varNode	varNode_copy (varNode x)
void	varNode_free ( varNode x)
cstring	interfaceNode_unparse (interfaceNode x)
void	interfaceNode_free ( interfaceNode x)
void	lsymbol_setbool (lsymbol s)
lsymbol	lsymbol_getbool ()
lsymbol	lsymbol_getBool ()
lsymbol	lsymbol_getFALSE ()
lsymbol	lsymbol_getTRUE ()

---

Function Documentation

termNode CollapseInfixTermNode ( termNode secondary, termNodeList infix )

Definition at line 3811 of file abstract.c. { termNode left = secondary; termNodeList_elements (infix, node) { termNodeList_addl (node->args, termNode_copySafe (left)); left = node; /* computePossibleSorts (left); */ } end_termNodeList_elements; return (left); }

void LCLBuiltins ( void )

Definition at line 216 of file abstract.c. { typeInfo ti = (typeInfo) dmalloc (sizeof (*ti)); varInfo vi = (varInfo) dmalloc (sizeof (*vi)); /* immutable type bool; uses CTrait; constant bool FALSE = false; constant bool TRUE = true; */ /* the following defines the builtin LSL sorts and operators */ LCLBootstrap (); /* now LCL builtin proper */ /* do "immutable type bool;" */ ti->id = ltoken_copy (ltoken_bool); ltoken_setCode (ti->id, LLT_TYPEDEF_NAME); ltoken_setIdType (ti->id, SID_TYPE); ti->modifiable = FALSE; ti->abstract = TRUE; ti->basedOn = sort_bool; ti->export = FALSE; /* this wasn't set (detected by lclint) */ symtable_enterType (g_symtab, ti); /* do "constant bool FALSE = false;" */ vi->id = ltoken_createType (simpleId, SID_VAR, lsymbol_fromChars ("FALSE")); vi->kind = VRK_CONST; vi->sort = sort_bool; vi->export = TRUE; (void) symtable_enterVar (g_symtab, vi); /* do "constant bool TRUE = true;" */ /* vi->id = ltoken_copy (vi->id); */ ltoken_setText (vi->id, lsymbol_fromChars ("TRUE")); (void) symtable_enterVar (g_symtab, vi); varInfo_free (vi); importCTrait (); }

cstring abstBodyNode_unparse ( abstBodyNode n )

Definition at line 2843 of file abstract.c. Referenced by abstractNode_unparse(). { if (n != (abstBodyNode) 0) { return (lclPredicateNode_unparse (n->typeinv)); } return cstring_undefined; }

cstring abstBodyNode_unparseExposed ( abstBodyNode n )

Definition at line 2853 of file abstract.c. Referenced by declaratorInvNode_unparse(). { if (n != (abstBodyNode) 0) { return (message ("%q", lclPredicateNode_unparse (n->typeinv))); } return cstring_undefined; }

cstring abstractNode_unparse ( abstractNode n )

Definition at line 2777 of file abstract.c. Referenced by typeNode_unparse(). { if (n != (abstractNode) 0) { cstring s; if (n->isMutable) s = cstring_makeLiteral ("mutable"); else s = cstring_makeLiteral ("immutable"); return (message ("%q type %s%q;", s, ltoken_getRawString (n->name), abstBodyNode_unparse (n->body))); } return cstring_undefined; }

void abstract_init ( )

Definition at line 109 of file abstract.c. { typeInfo ti = (typeInfo) dmalloc (sizeof (*ti)); nameNode nn; ltoken dom, range; sigNode sign; opFormNode opform; ltokenList domain = ltokenList_new (); ltokenList domain2; equalSymbol = lsymbol_fromChars ("="); eqSymbol = lsymbol_fromChars ("\\eq"); /* ** not: cstring_toCharsSafe (context_getBoolName ()) ** we use the hard wired "bool" name. */ lsymbol_bool = lsymbol_fromChars ("bool"); lsymbol_Bool = lsymbol_fromChars ("Bool"); lsymbol_TRUE = lsymbol_fromChars ("TRUE"); lsymbol_FALSE = lsymbol_fromChars ("FALSE"); ConditionalSymbol = lsymbol_fromChars ("if__then__else__"); /* generate operators for ** __ \not, __ \implies __ , __ \and __, __ \or __ */ range = ltoken_create (simpleId, lsymbol_bool); dom = ltoken_create (simpleId, lsymbol_bool); ltokenList_addh (domain, ltoken_copy (dom)); domain2 = ltokenList_copy (domain); /* moved this here (before release) */ sign = makesigNode (ltoken_undefined, domain, ltoken_copy (range)); opform = makeOpFormNode (ltoken_undefined, OPF_ANYOPM, opFormUnion_createAnyOp (ltoken_not), ltoken_undefined); nn = makeNameNodeForm (opform); symtable_enterOp (g_symtab, nn, sign); ltokenList_addh (domain2, dom); sign = makesigNode (ltoken_undefined, domain2, range); opform = makeOpFormNode (ltoken_undefined, OPF_MANYOPM, opFormUnion_createAnyOp (ltoken_and), ltoken_undefined); nn = makeNameNodeForm (opform); symtable_enterOp (g_symtab, nn, sigNode_copy (sign)); opform = makeOpFormNode (ltoken_undefined, OPF_MANYOPM, opFormUnion_createAnyOp (ltoken_or), ltoken_undefined); nn = makeNameNodeForm (opform); symtable_enterOp (g_symtab, nn, sigNode_copy (sign)); opform = makeOpFormNode (ltoken_undefined, OPF_MANYOPM, opFormUnion_createAnyOp (ltoken_implies), ltoken_undefined); nn = makeNameNodeForm (opform); symtable_enterOp (g_symtab, nn, sign); /* from lclscanline.c's init procedure */ /* comment out so we can add in lclinit.lci: synonym double float */ /* ReserveToken (FLOAT, "float"); */ /* But we need to make the scanner parse "float" not as a simpleId, but as a TYPEDEF_NAME. This is done later in abstract_init */ ti->id = ltoken_createType (LLT_TYPEDEF_NAME, SID_TYPE, lsymbol_fromChars ("float")); ti->modifiable = FALSE; ti->abstract = FALSE; ti->export = FALSE; /* this is implicit, not exported */ ti->basedOn = sort_float; symtable_enterType (g_symtab, ti); }

lsymbol checkAndEnterTag ( tagKind k, ltoken opttagid )

Definition at line 5197 of file abstract.c. Referenced by makeForwardstrOrUnionNode(). { /* should be tagKind, instead of int */ tagInfo t; sort sort = sort_makeNoSort (); if (!ltoken_isUndefined (opttagid)) { switch (k) { case TAG_FWDSTRUCT: case TAG_STRUCT: sort = sort_makeStr (opttagid); break; case TAG_FWDUNION: case TAG_UNION: sort = sort_makeUnion (opttagid); break; case TAG_ENUM: sort = sort_makeEnum (opttagid); break; } /* see if it is already in symbol table */ t = symtable_tagInfo (g_symtab, ltoken_getText (opttagid)); if (tagInfo_exists (t)) { if (t->kind == TAG_FWDUNION || t->kind == TAG_FWDSTRUCT) { /* this is fine, for mutually recursive types */ } else { /* this is not good, complain later */ cstring s; switch (k) { case TAG_ENUM: s = cstring_makeLiteral ("Enum"); break; case TAG_STRUCT: case TAG_FWDSTRUCT: s = cstring_makeLiteral ("Struct"); break; case TAG_UNION: case TAG_FWDUNION: s = cstring_makeLiteral ("Union"); break; } t->sort = sort; t->kind = k; lclerror (opttagid, message ("Tag redefined: %q %s", s, ltoken_getRawString (opttagid))); } ltoken_free (opttagid); } else { tagInfo newnode = (tagInfo) dmalloc (sizeof (*newnode)); newnode->sort = sort; newnode->kind = k; newnode->id = opttagid; newnode->imported = FALSE; newnode->content.decls = stDeclNodeList_new (); (void) symtable_enterTag (g_symtab, newnode); } } return sort_getLsymbol (sort); }

void checkBrackets ( ltoken lb, ltoken rb )

Definition at line 1120 of file abstract.c. { /* no attempt at error recovery...not really necessary */ cstring tname; tname = ltoken_getRawString (lb); if (!cstring_equalLit (tname, "<")) { cylerror (cstring_toCharsSafeO (message ("Invalid import token: %s", tname))); } tname = ltoken_getRawString (rb); if (!cstring_equalLit (tname, ">")) { cylerror (cstring_toCharsSafeO (message ("Invalid import token: %s", tname))); } }

cstring claimNode_unparse ( claimNode c )

Definition at line 4358 of file abstract.c. Referenced by exportNode_unparse(). { if (c != (claimNode) 0) { cstring s = message ("claims (%q)%q{\n%q", paramNodeList_unparse (c->params), varDeclarationNodeList_unparse (c->globals), lclPredicateNode_unparse (c->require)); if (c->body != NULL) { s = message ("%qbody {%q}\n", s, programNode_unparse (c->body)); } s = message ("%q%q}\n", s, lclPredicateNode_unparse (c->ensures)); return s; } return cstring_undefined; }

interfaceNodeList consInterfaceNode ( interfaceNode n, interfaceNodeList ns )

Definition at line 296 of file abstract.c. { /* n is never empty, but ns may be empty */ interfaceNodeList_addl (ns, n); return (ns); }

cstring constDeclarationNode_unparse ( constDeclarationNode x )

Definition at line 716 of file abstract.c. Referenced by exportNode_unparse(), and privateNode_unparse(). { if (x != (constDeclarationNode) 0) { return (message ("constant %q %q", lclTypeSpecNode_unparse (x->type), initDeclNodeList_unparse (x->decls))); } return cstring_undefined; }

void declaratorInvNode_free ( declaratorInvNode x )

Definition at line 5768 of file abstract.c. Referenced by declaratorInvNodeList_free(). { if (x != NULL) { declaratorNode_free (x->declarator); abstBodyNode_free (x->body); sfree (x); } }

cstring declaratorInvNode_unparse ( declaratorInvNode d )

Definition at line 2836 of file abstract.c. { return (message ("%q%q", declaratorNode_unparse (d->declarator), abstBodyNode_unparseExposed (d->body))); }

declaratorNode declaratorNode_copy ( declaratorNode x )

Definition at line 2252 of file abstract.c. Referenced by doDeclareConstant(), and doDeclareVar(). { declaratorNode ret = (declaratorNode) dmalloc (sizeof (*ret)); ret->type = typeExpr_copy (x->type); ret->id = ltoken_copy (x->id); ret->isRedecl = x->isRedecl; return (ret); }

void declaratorNode_free ( declaratorNode x )

Definition at line 5728 of file abstract.c. Referenced by declaratorInvNode_free(), declaratorNodeList_free(), fcnNode_free(), and initDeclNode_free(). { if (x != NULL) { typeExpr_free (x->type); ltoken_free (x->id); sfree (x); } }

cstring declaratorNode_unparse ( declaratorNode x )

Definition at line 2246 of file abstract.c. Referenced by declaratorNodeList_unparse(), fcnNode_unparse(), initDeclNodeList_unparse(), lhType(), and taggedUnionNode_unparse(). { return (typeExpr_unparse (x->type)); }

cstring declaratorNode_unparseCode ( declaratorNode x )

Definition at line 2351 of file abstract.c. Referenced by lhType(). { return (typeExpr_unparseCode (x->type)); }

void declareForwardType ( declaratorNode declare )

Definition at line 194 of file abstract.c. { typeInfo ti = (typeInfo) dmalloc (sizeof (*ti)); sort tsort, handle; lsymbol typedefname; typedefname = ltoken_getText (declare->id); ti->id = ltoken_copy (declare->id); ltoken_setCode (ti->id, LLT_TYPEDEF_NAME); ltoken_setIdType (ti->id, SID_TYPE); ti->modifiable = FALSE; ti->abstract = FALSE; tsort = lclTypeSpecNode2sort (exposedType); handle = typeExpr2ptrSort (tsort, declare->type); ti->basedOn = sort_makeSyn (declare->id, handle, typedefname); ti->export = FALSE; symtable_enterType (g_symtab, ti); }

void enteringClaimScope ( paramNodeList params, globalList g )

Definition at line 5446 of file abstract.c. { scopeInfo si = (scopeInfo) dmalloc (sizeof (*si)); pairNodeList globals; lclTypeSpecNode paramtype; typeExpr paramdecl; sort sort; globals = globalList_toPairNodeList (g); /* push new claim scope */ si->kind = SPE_CLAIM; symtable_enterScope (g_symtab, si); /* push onto symbol table the formal parameters of this function, together with their respective sorts */ paramNodeList_elements (params, param) { paramdecl = param->paramdecl; paramtype = param->type; if (paramdecl != (typeExpr) 0 && paramtype != (lclTypeSpecNode) 0) { varInfo vi = (varInfo) dmalloc (sizeof (*vi)); sort = lclTypeSpecNode2sort (paramtype); sort = sort_makeFormal (sort); vi->sort = typeExpr2ptrSort (sort, paramdecl); vi->id = ltoken_copy (extractDeclarator (paramdecl)); vi->kind = VRK_PARAM; vi->export = TRUE; (void) symtable_enterVar (g_symtab, vi); varInfo_free (vi); } } end_paramNodeList_elements; /* push onto symbol table the global variables declared in this function, together with their respective sorts */ pairNodeList_elements (globals, g2) { varInfo vi = (varInfo) dmalloc (sizeof (*vi)); vi->id = ltoken_copy (g2->tok); vi->kind = VRK_GLOBAL; vi->sort = g2->sort; vi->export = TRUE; /* should catch duplicates in formals */ (void) symtable_enterVar (g_symtab, vi); varInfo_free (vi); } end_pairNodeList_elements; pairNodeList_free (globals); /* should not free it here! ltoken_free (claimId); @*/ }

void enteringFcnScope ( lclTypeSpecNode t, declaratorNode d, globalList g )

Definition at line 5353 of file abstract.c. { scopeInfo si = (scopeInfo) dmalloc (sizeof (*si)); varInfo vi = (varInfo) dmalloc (sizeof (*vi)); sort returnSort; ltoken result = ltoken_copy (ltoken_id); pairNodeList paramPairs, globals; fctInfo fi = (fctInfo) dmalloc (sizeof (*fi)); signNode sign = (signNode) dmalloc (sizeof (*sign)); sortList domain = sortList_new (); unsigned int key; paramPairs = extractParams (d->type); returnSort = extractReturnSort (t, d); globals = globalList_toPairNodeList (g); sign->tok = ltoken_undefined; sign->range = returnSort; key = MASH (0, sort_getLsymbol (returnSort)); pairNodeList_elements (paramPairs, p) { sortList_addh (domain, p->sort); key = MASH (key, sort_getLsymbol (p->sort)); } end_pairNodeList_elements; sign->domain = domain; sign->key = key; /* push fcn onto symbol table stack first */ fi->id = ltoken_copy (d->id); fi->export = TRUE; fi->signature = sign; fi->globals = globals; (void) symtable_enterFct (g_symtab, fi); /* push new fcn scope */ si->kind = SPE_FCN; symtable_enterScope (g_symtab, si); /* add "result" with return type to current scope */ ltoken_setText (result, lsymbol_fromChars ("result")); vi->id = result; vi->sort = sort_makeFormal (returnSort); /* make appropriate values */ vi->kind = VRK_PARAM; vi->export = TRUE; (void) symtable_enterVar (g_symtab, vi); /* ** evs - 4 Mar 1995 ** pust globals first (they are in outer scope) */ /* push onto symbol table the global variables declared in this function, together with their respective sorts */ pairNodeList_elements (globals, gl) { ltoken_free (vi->id); vi->id = ltoken_copy (gl->tok); vi->kind = VRK_GLOBAL; vi->sort = gl->sort; (void) symtable_enterVar (g_symtab, vi); } end_pairNodeList_elements; /* ** could enter a new scope; instead, warn when variable shadows global ** that is used */ /* ** push onto symbol table the formal parameters of this function, ** together with their respective sorts */ pairNodeList_elements (paramPairs, pair) { ltoken_free (vi->id); vi->id = ltoken_copy (pair->tok); vi->sort = pair->sort; vi->kind = VRK_PARAM; (void) symtable_enterVar (g_symtab, vi); } end_pairNodeList_elements; pairNodeList_free (paramPairs); varInfo_free (vi); }

cstring enumSpecNode_unparse ( enumSpecNode n )

Definition at line 1887 of file abstract.c. Referenced by lclTypeSpecNode_unparse(). { if (n != (enumSpecNode) 0) { cstring s = cstring_makeLiteral ("enum "); if (!ltoken_isUndefined (n->opttagid)) { s = message ("%q%s ", s, ltoken_getRawString (n->opttagid)); } s = message ("%q{%q}", s, printLeaves2 (n->enums)); return s; } return cstring_undefined; }

cstring exportNode_unparse ( exportNode n )

Definition at line 502 of file abstract.c. { if (n != (exportNode) 0) { switch (n->kind) { case XPK_CONST: return (message ("%q\n", constDeclarationNode_unparse (n->content.constdeclaration))); case XPK_VAR: return (message ("%q\n", varDeclarationNode_unparse (n->content.vardeclaration))); case XPK_TYPE: return (message ("%q\n", typeNode_unparse (n->content.type))); case XPK_FCN: return (fcnNode_unparse (n->content.fcn)); case XPK_CLAIM: return (claimNode_unparse (n->content.claim)); case XPK_ITER: return (iterNode_unparse (n->content.iter)); default: llfatalbug (message ("exportNode_unparse: unknown kind: %d", (int) n->kind)); } } return cstring_undefined; }

cstring exposedNode_unparse ( exposedNode n )

Definition at line 2814 of file abstract.c. Referenced by typeNode_unparse(). { if (n != (exposedNode) 0) { return (message ("typedef %q %q;", lclTypeSpecNode_unparse (n->type), declaratorInvNodeList_unparse (n->decls))); } return cstring_undefined; }

void fcnNode_free ( fcnNode f )

Definition at line 5749 of file abstract.c. Referenced by doDeclareConstant(), doDeclareVar(), and fcnNodeList_free(). { if (f != NULL) { lclTypeSpecNode_free (f->typespec); declaratorNode_free (f->declarator); globalList_free (f->globals); varDeclarationNodeList_free (f->inits); letDeclNodeList_free (f->lets); lclPredicateNode_free (f->checks); lclPredicateNode_free (f->require); lclPredicateNode_free (f->claim); lclPredicateNode_free (f->ensures); modifyNode_free (f->modify); ltoken_free (f->name); sfree (f); } }

fcnNode fcnNode_fromDeclarator ( lclTypeSpecNode t, declaratorNode d )

Definition at line 2895 of file abstract.c. Referenced by doDeclareConstant(), doDeclareVar(), and makeAbstBodyNode2(). { return (makeFcnNode (QU_UNKNOWN, t, d, varDeclarationNodeList_new (), varDeclarationNodeList_new (), letDeclNodeList_new (), (lclPredicateNode) 0, (lclPredicateNode) 0, (modifyNode) 0, (lclPredicateNode) 0, (lclPredicateNode) 0)); }

cstring fcnNode_unparse ( fcnNode f )

Definition at line 641 of file abstract.c. Referenced by exportNode_unparse(), and privateNode_unparse(). { if (f != (fcnNode) 0) { return (message ("%q %q%q{\n%q%q%q%q%q%q}\n", lclTypeSpecNode_unparse (f->typespec), declaratorNode_unparse (f->declarator), varDeclarationNodeList_unparse (f->globals), varDeclarationNodeList_unparse (f->inits), letDeclNodeList_unparse (f->lets), lclPredicateNode_unparse (f->require), modifyNode_unparse (f->modify), lclPredicateNode_unparse (f->ensures), lclPredicateNode_unparse (f->claim))); } return cstring_undefined; }

void importNode_free ( importNode x )

Definition at line 5877 of file abstract.c. Referenced by importNodeList_free(). { sfree (x); }

importNode importNode_makeBracketed ( ltoken t )

Definition at line 1070 of file abstract.c. { importNode imp = (importNode) dmalloc (sizeof (*imp)); imp->kind = IMPBRACKET; imp->val = t; return (imp); }

importNode importNode_makePlain ( ltoken t )

Definition at line 1060 of file abstract.c. { importNode imp = (importNode) dmalloc (sizeof (*imp)); imp->kind = IMPPLAIN; imp->val = t; return (imp); }

importNode importNode_makeQuoted ( ltoken t )

Definition at line 1093 of file abstract.c. { importNode imp = (importNode) dmalloc (sizeof (*imp)); cstring q = extractQuote (cstring_copy (ltoken_getRawString (t))); imp->kind = IMPQUOTE; ltoken_setRawText (t, lsymbol_fromChars (cstring_toCharsSafe (q))); imp->val = t; cstring_free (q); return (imp); }

void initDeclNode_free ( initDeclNode x )

Definition at line 5882 of file abstract.c. Referenced by initDeclNodeList_free(). { if (x != NULL) { declaratorNode_free (x->declarator); termNode_free (x->value); sfree (x); } }

bool initDeclNode_isRedeclaration ( initDeclNode d )

Definition at line 5810 of file abstract.c. Referenced by doDeclareVar(). { return (d->declarator->isRedecl); }

void interfaceNode_free ( interfaceNode x )

Definition at line 6184 of file abstract.c. Referenced by interfaceNodeList_free(). { if (x != NULL) { switch (x->kind) { case INF_IMPORTS: importNodeList_free (x->content.imports); break; case INF_USES: traitRefNodeList_free (x->content.uses); break; case INF_EXPORT: exportNode_free (x->content.export); break; case INF_PRIVATE: privateNode_free (x->content.private); break; } sfree (x); } }

interfaceNode interfaceNode_makeClaim ( claimNode x )

Definition at line 419 of file abstract.c. { interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); exportNode e = (exportNode) dmalloc (sizeof (*e)); e->kind = XPK_CLAIM; e->content.claim = x; i->kind = INF_EXPORT; i->content.export = e; return (i); }

interfaceNode interfaceNode_makeConst ( constDeclarationNode x )

Definition at line 345 of file abstract.c. { interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); exportNode e = (exportNode) dmalloc (sizeof (*e)); e->kind = XPK_CONST; e->content.constdeclaration = x; i->kind = INF_EXPORT; i->content.export = e; return (i); }

interfaceNode interfaceNode_makeFcn ( fcnNode x )

Definition at line 397 of file abstract.c. { interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); exportNode e = (exportNode) dmalloc (sizeof (*e)); e->kind = XPK_FCN; e->content.fcn = x; i->kind = INF_EXPORT; i->content.export = e; if (context_msgLh ()) { llassert (x->typespec != NULL); llassert (x->declarator != NULL); lhOutLine (lhFunction (x->typespec, x->declarator)); } return (i); }

interfaceNode interfaceNode_makeIter ( iterNode x )

Definition at line 432 of file abstract.c. { interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); exportNode e = (exportNode) dmalloc (sizeof (*e)); e->kind = XPK_ITER; e->content.iter = x; i->kind = INF_EXPORT; i->content.export = e; return (i); }

interfaceNode interfaceNode_makePrivConst ( constDeclarationNode x )

Definition at line 445 of file abstract.c. { interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); privateNode e = (privateNode) dmalloc (sizeof (*e)); e->kind = PRIV_CONST; e->content.constdeclaration = x; i->kind = INF_PRIVATE; i->content.private = e; return (i); }

interfaceNode interfaceNode_makePrivFcn ( fcnNode x )

Definition at line 484 of file abstract.c. { interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); privateNode e = (privateNode) dmalloc (sizeof (*e)); /* ** bug detected by lclint enum checking ** e->kind = XPK_FCN; */ e->kind = PRIV_FUNCTION; e->content.fcn = x; i->kind = INF_PRIVATE; i->content.private = e; return (i); }

interfaceNode interfaceNode_makePrivType ( typeNode x )

Definition at line 471 of file abstract.c. { interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); privateNode e = (privateNode) dmalloc (sizeof (*e)); e->kind = PRIV_TYPE; e->content.type = x; i->kind = INF_PRIVATE; i->content.private = e; return (i); }

interfaceNode interfaceNode_makePrivVar ( varDeclarationNode x )

Definition at line 458 of file abstract.c. { interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); privateNode e = (privateNode) dmalloc (sizeof (*e)); e->kind = PRIV_VAR; e->content.vardeclaration = x; i->kind = INF_PRIVATE; i->content.private = e; return (i); }

interfaceNode interfaceNode_makeType ( typeNode x )

Definition at line 378 of file abstract.c. { interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); exportNode e = (exportNode) dmalloc (sizeof (*e)); e->kind = XPK_TYPE; e->content.type = x; i->kind = INF_EXPORT; i->content.export = e; if (context_msgLh ()) { lhOutLine (lhType (x)); } return (i); }

interfaceNode interfaceNode_makeVar ( varDeclarationNode x )

Definition at line 359 of file abstract.c. { interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); exportNode e = (exportNode) dmalloc (sizeof (*e)); e->kind = XPK_VAR; e->content.vardeclaration = x; i->kind = INF_EXPORT; i->content.export = e; if (context_msgLh ()) { lhOutLine (lhVarDecl (x->type, x->decls, x->qualifier)); } return (i); }

cstring interfaceNode_unparse ( interfaceNode x )

Definition at line 6160 of file abstract.c. { if (x != NULL) { switch (x->kind) { case INF_IMPORTS: return (message ("[imports] %q", importNodeList_unparse (x->content.imports))); case INF_USES: return (message ("[uses] %q", traitRefNodeList_unparse (x->content.uses))); case INF_EXPORT: return (message ("[export] %q", exportNode_unparse (x->content.export))); case INF_PRIVATE: return (message ("[private] %q", privateNode_unparse (x->content.private))); } BADBRANCH; } else { return (cstring_makeLiteral ("<interface node undefined>")); } }

cstring iterNode_unparse ( iterNode i )

Definition at line 629 of file abstract.c. Referenced by exportNode_unparse(). { if (i != (iterNode) 0) { return (message ("iter %s %q", ltoken_unparse (i->name), paramNodeList_unparse (i->params))); } return cstring_undefined; }

sort lclTypeSpecNode2sort ( lclTypeSpecNode type )

Definition at line 5172 of file abstract.c. Referenced by declareForwardType(), enteringClaimScope(), makeConstDeclarationNode(), makeLetDeclNode(), makeModifyNodeRef(), makeUnchangedTermNode2(), makeVarDeclarationNode(), makeVarNode(), and makestrOrUnionNode(). { if (type != (lclTypeSpecNode) 0) { switch (type->kind) { case LTS_TYPE: llassert (type->content.type != NULL); return sort_makePtrN (type->content.type->sort, type->pointers); case LTS_STRUCTUNION: llassert (type->content.structorunion != NULL); return sort_makePtrN (type->content.structorunion->sort, type->pointers); case LTS_ENUM: llassert (type->content.enumspec != NULL); return sort_makePtrN (type->content.enumspec->sort, type->pointers); case LTS_CONJ: return (lclTypeSpecNode2sort (type->content.conj->a)); } } return (sort_makeNoSort ()); }

lclTypeSpecNode lclTypeSpecNode_addQual ( lclTypeSpecNode n, qual q )

Definition at line 1723 of file abstract.c. { llassert (lclTypeSpecNode_isDefined (n)); n->quals = qualList_add (n->quals, q); return n; }

lclTypeSpecNode lclTypeSpecNode_copy ( lclTypeSpecNode n )

Definition at line 5616 of file abstract.c. Referenced by paramNode_copy(), and storeRefNode_copy(). { if (n != NULL) { switch (n->kind) { case LTS_CONJ: return (makeLclTypeSpecNodeConj (lclTypeSpecNode_copy (n->content.conj->a), lclTypeSpecNode_copy (n->content.conj->b))); case LTS_TYPE: return (makeLclTypeSpecNodeType (CTypesNode_copy (n->content.type))); case LTS_STRUCTUNION: return (makeLclTypeSpecNodeSU (strOrUnionNode_copy (n->content.structorunion))); case LTS_ENUM: return (makeLclTypeSpecNodeEnum (enumSpecNode_copy (n->content.enumspec))); } } return NULL; }

ltoken lclTypeSpecNode_errorToken ( lclTypeSpecNode t )

Definition at line 889 of file abstract.c. Referenced by makeModifyNodeRef(), and makeUnchangedTermNode2(). { if (t != (lclTypeSpecNode) 0) { switch (t->kind) { case LTS_TYPE: { llassert (t->content.type != NULL); if (ltokenList_empty (t->content.type->ctypes)) break; else return (ltokenList_head (t->content.type->ctypes)); } case LTS_STRUCTUNION: llassert (t->content.structorunion != NULL); return t->content.structorunion->tok; case LTS_ENUM: llassert (t->content.enumspec != NULL); return t->content.enumspec->tok; case LTS_CONJ: return (lclTypeSpecNode_errorToken (t->content.conj->a)); } } return ltoken_undefined; }

cstring lclTypeSpecNode_unparse ( lclTypeSpecNode n )

Definition at line 1731 of file abstract.c. Referenced by paramNode_unparse(). { if (n != (lclTypeSpecNode) 0) { switch (n->kind) { case LTS_TYPE: llassert (n->content.type != NULL); return (printLeaves (n->content.type->ctypes)); case LTS_STRUCTUNION: return (strOrUnionNode_unparse (n->content.structorunion)); case LTS_ENUM: return (enumSpecNode_unparse (n->content.enumspec)); case LTS_CONJ: return (lclTypeSpecNode_unparse (n->content.conj->a)); default: llfatalbug (message ("lclTypeSpecNode_unparse: unknown lclTypeSpec kind: %d", (int) n->kind)); } } return cstring_undefined; }

cstring lclTypeSpecNode_unparseComments ( lclTypeSpecNode typespec )

Definition at line 3458 of file abstract.c. Referenced by paramNode_unparseComments(). { if (typespec != (lclTypeSpecNode) 0) { cstring s = qualList_toCComments (typespec->quals); switch (typespec->kind) { case LTS_TYPE: { llassert (typespec->content.type != NULL); return (cstring_concatFree (s, printLeaves (typespec->content.type->ctypes))); } case LTS_ENUM: { bool first = TRUE; enumSpecNode n = typespec->content.enumspec; s = cstring_concatFree (s, cstring_makeLiteral ("enum")); llassert (n != NULL); if (!ltoken_isUndefined (n->opttagid)) { s = message ("%q %s", s, ltoken_unparse (n->opttagid)); } s = message ("%q {", s); ltokenList_elements (n->enums, e) { if (first) { first = FALSE; s = message ("%q%s", s, ltoken_getRawString (e)); } else s = message ("%q, %s", s, ltoken_getRawString (e)); } end_ltokenList_elements; return (message ("%q}", s)); } case LTS_STRUCTUNION: { strOrUnionNode n = typespec->content.structorunion; stDeclNodeList decls; llassert (n != NULL); switch (n->kind) { case SU_STRUCT: s = cstring_concatFree (s, cstring_makeLiteral ("struct ")); /*@switchbreak@*/ break; case SU_UNION: s = cstring_concatFree (s, cstring_makeLiteral ("union ")); /*@switchbreak@*/ break; } if (!ltoken_isUndefined (n->opttagid)) { if (stDeclNodeList_size (n->structdecls) == 0) { return (message ("%q%s", s, ltoken_unparse (n->opttagid))); } s = message ("%q%s {\n\2\1", s, ltoken_unparse (n->opttagid)); } else { s = message ("%q{\n\2\1", s); } decls = n->structdecls; stDeclNodeList_elements (decls, f) { s = message ("%q%q\1%q;\n\1", s, lclTypeSpecNode_unparseComments (f->lcltypespec), declaratorNodeList_unparse (f->declarators)); } end_stDeclNodeList_elements; return (message ("%q\3}", s)); } case LTS_CONJ: { cstring_free (s); return (message ("%q /*@alt %q@*/", lclTypeSpecNode_unparseComments (typespec->content.conj->a), lclTypeSpecNode_unparseAltComments (typespec->content.conj->b))); } BADDEFAULT; } } else { llcontbuglit ("lclTypeSpecNode_unparseComments: null typespec"); return cstring_undefined; } BADEXIT; }

void letDeclNode_free ( letDeclNode x )

Definition at line 5892 of file abstract.c. Referenced by letDeclNodeList_free(). { if (x != NULL) { lclTypeSpecNode_free (x->sortspec); termNode_free (x->term); ltoken_free (x->varid); sfree (x); } }

lslOp lslOp_copy ( lslOp x )

Definition at line 5778 of file abstract.c. Referenced by parseOpLine(). { return (makelslOpNode (nameNode_copy (x->name), x->signature)); }

bool lslOp_equal ( lslOp x, lslOp y )

Definition at line 5703 of file abstract.c. { return ((x == y) || ((x != 0) && (y != 0) && sameNameNode (x->name, y->name) && sigNode_equal (x->signature, y->signature))); }

void lslOp_free ( lslOp x )

Definition at line 5711 of file abstract.c. Referenced by lslOpSet_free(), and lslOpSet_insert(). { nameNode_free (x->name); sfree (x); }

cstring lslOp_unparse ( lslOp x )

Definition at line 4904 of file abstract.c. { char *s = mstring_createEmpty (); if (x != (lslOp) 0) { s = mstring_concatFree (s, cstring_toCharsSafe (nameNode_unparse (x->name))); if (x->signature != (sigNode) 0) { s = mstring_concatFree (s, cstring_toCharsSafe (sigNode_unparse (x->signature))); } } return cstring_fromCharsO (s); }

lsymbol lsymbol_getBool ( )

Definition at line 6392 of file abstract.c. Referenced by symtable_enterType(). { return lsymbol_Bool; }

lsymbol lsymbol_getFALSE ( )

Definition at line 6397 of file abstract.c. Referenced by symtable_enterVar(). { return lsymbol_FALSE; }

lsymbol lsymbol_getTRUE ( )

Definition at line 6402 of file abstract.c. Referenced by symtable_enterVar(). { return lsymbol_TRUE; }

lsymbol lsymbol_getbool ( )

Definition at line 6387 of file abstract.c. Referenced by symtable_enterType(), and symtable_new(). { return lsymbol_bool; }

void lsymbol_setbool ( lsymbol s )

Definition at line 6382 of file abstract.c. Referenced by sort_init(). { lsymbol_bool = s; }

bool ltoken_similar ( ltoken t1, ltoken t2 )

Definition at line 603 of file abstract.c. Referenced by ltokenList_equal(), sameNameNode(), and sigNode_equal(). { lsymbol sym1 = ltoken_getText (t1); lsymbol sym2 = ltoken_getText (t2); if (sym1 == sym2) { return TRUE; } if ((sym1 == eqSymbol && sym2 == equalSymbol) || (sym2 == eqSymbol && sym1 == equalSymbol)) { return TRUE; } if ((sym1 == lsymbol_bool && sym2 == lsymbol_Bool) || (sym2 == lsymbol_bool && sym1 == lsymbol_Bool)) { return TRUE; } return FALSE; }

abstBodyNode makeAbstBodyNode ( ltoken t, fcnNodeList f )

Definition at line 3108 of file abstract.c. { abstBodyNode x = (abstBodyNode) dmalloc (sizeof (*x)); x->tok = t; x->typeinv = (lclPredicateNode)0; x->fcns = f; return (x); }

abstBodyNode makeAbstBodyNode2 ( ltoken t, ltokenList ops )

Definition at line 3130 of file abstract.c. { abstBodyNode x = (abstBodyNode) dmalloc (sizeof (*x)); x->tok = t; x->typeinv = (lclPredicateNode) 0; x->fcns = fcnNodeList_new (); ltokenList_elements (ops, op) { x->fcns = fcnNodeList_add (x->fcns, fcnNode_fromDeclarator (lclTypeSpecNode_undefined, makeUnknownDeclaratorNode (ltoken_copy (op)))); } end_ltokenList_elements; ltokenList_free (ops); return (x); }

abstractNode makeAbstractNode ( ltoken t, ltoken name, bool isMutable, bool isRefCounted, abstBodyNode a )

Definition at line 2744 of file abstract.c. { abstractNode n = (abstractNode) dmalloc (sizeof (*n)); sort handle; typeInfo ti = (typeInfo) dmalloc (sizeof (*ti)); n->tok = t; n->isMutable = isMutable; n->name = name; n->body = a; n->isRefCounted = isRefCounted; if (isMutable) handle = sort_makeMutable (name, ltoken_getText (name)); else handle = sort_makeImmutable (name, ltoken_getText (name)); n->sort = handle; ti->id = ltoken_createType (ltoken_getCode (ltoken_typename), SID_TYPE, ltoken_getText (name)); ti->modifiable = isMutable; ti->abstract = TRUE; ti->basedOn = handle; ti->export = TRUE; symtable_enterType (g_symtab, ti); return n; }

typeNode makeAbstractTypeNode ( abstractNode x )

Definition at line 1035 of file abstract.c. { typeNode n = (typeNode) dmalloc (sizeof (*n)); n->kind = TK_ABSTRACT; n->content.abstract = x; return (n); }

typeExpr makeArrayNode ( typeExpr x, arrayQualNode a )

Definition at line 2518 of file abstract.c. { if (x != (typeExpr)0 && (x->kind == TEXPR_FCN && (x->wrapped == 0))) { /* ** Spurious errors reported here, because of referencing ** in makeArrayNode. */ /*@i3@*/ x->content.function.returntype = makeArrayNode (x, a); /*@i1@*/ return x; } else { typeExpr y = (typeExpr) dmalloc (sizeof (*y)); y->wrapped = 0; y->kind = TEXPR_ARRAY; if (a == (arrayQualNode) 0) { y->content.array.size = (termNode) 0; } else { y->content.array.size = a->term; ltoken_free (a->tok); sfree (a); } y->content.array.elementtype = x; y->sort = sort_makeNoSort (); return (y); } }

arrayQualNode makeArrayQualNode ( ltoken t, termNode term )

Definition at line 3058 of file abstract.c. { arrayQualNode x = (arrayQualNode) dmalloc (sizeof (*x)); x->tok = t; x->term = term; return (x); }

CTypesNode makeCTypesNode ( CTypesNode ctypes, ltoken ct )

Definition at line 5023 of file abstract.c. { /*@only@*/ CTypesNode newnode; lsymbol sortname; bits sortbits; if (ctypes == (CTypesNode) NULL) { newnode = (CTypesNode) dmalloc (sizeof (*newnode)); newnode->intfield = 0; newnode->ctypes = ltokenList_new (); newnode->sort = sort_makeNoSort (); } else { newnode = ctypes; } if ((ltoken_getIntField (ct) & newnode->intfield) != 0) { lclerror (ct, message ("Duplicate type specifier ignored: %s", cstring_fromChars (lsymbol_toChars (lclctype_toSortDebug (ltoken_getIntField (ct)))))); /* evs --- don't know how to generator this error */ /* Use previous value, to keep things consistent */ ltoken_free (ct); return newnode; } sortbits = newnode->intfield | ltoken_getIntField (ct); sortname = lclctype_toSort (sortbits); if (sortname == lsymbol_fromChars ("error")) { lclerror (ct, cstring_makeLiteral ("Invalid combination of type specifiers")); } else { newnode->intfield = sortbits; } ltokenList_addh (newnode->ctypes, ct); /* ** Sorts are assigned after CTypesNode is created during parsing, ** see bison grammar. */ return newnode; }

lclPredicateNode makeChecksNode ( ltoken t, lclPredicateNode n )

Definition at line 3016 of file abstract.c. { ltoken_free (n->tok); n->tok = t; n->kind = LPD_CHECKS; return (n); }

claimNode makeClaimNode ( ltoken id, paramNodeList p, globalList g, letDeclNodeList lets, lclPredicateNode requires, programNode b, lclPredicateNode ensures )

Definition at line 2980 of file abstract.c. { claimNode x = (claimNode) dmalloc (sizeof (*x)); x->name = id; x->params = p; x->globals = g; x->lets = lets; x->require = requires; x->body = b; x->ensures = ensures; return (x); }

constDeclarationNode makeConstDeclarationNode ( lclTypeSpecNode t, initDeclNodeList decls )

Definition at line 2556 of file abstract.c. { constDeclarationNode n = (constDeclarationNode) dmalloc (sizeof (*n)); sort s, s2, initValueSort; ltoken varid, errtok; termNode initValue; s = lclTypeSpecNode2sort (t); initDeclNodeList_elements (decls, init) { declaratorNode vdnode = init->declarator; varInfo vi = (varInfo) dmalloc (sizeof (*vi)); varid = ltoken_copy (vdnode->id); s2 = typeExpr2ptrSort (s, vdnode->type); initValue = init->value; if (termNode_isDefined (initValue) && !initValue->error_reported) { initValueSort = initValue->sort; /* should keep the arguments in order */ if (!sort_member_modulo_cstring (s2, initValue) && !initValue->error_reported) { errtok = termNode_errorToken (initValue); lclerror (errtok, message ("Constant %s declared type %q, initialized to %q: %q", ltoken_unparse (varid), sort_unparse (s2), sort_unparse (initValueSort), termNode_unparse (initValue))); } } vi->id = varid; vi->kind = VRK_CONST; vi->sort = s2; vi->export = TRUE; (void) symtable_enterVar (g_symtab, vi); varInfo_free (vi); } end_initDeclNodeList_elements; n->type = t; n->decls = decls; return n; }

declaratorInvNode makeDeclaratorInvNode ( declaratorNode d, abstBodyNode b )

Definition at line 2826 of file abstract.c. { declaratorInvNode n = (declaratorInvNode) dmalloc (sizeof (*n)); n->declarator = d; n->body = b; return (n); }

declaratorNode makeDeclaratorNode ( typeExpr t )

Definition at line 2185 of file abstract.c. { declaratorNode x = (declaratorNode) dmalloc (sizeof (*x)); x->id = ltoken_copy (extractDeclarator (t)); x->type = t; x->isRedecl = FALSE; return (x); }

lclPredicateNode makeEnsuresNode ( ltoken t, lclPredicateNode n )

Definition at line 3025 of file abstract.c. { ltoken_free (n->tok); n->tok = t; n->kind = LPD_ENSURES; return (n); }

enumSpecNode makeEnumSpecNode ( ltoken t, ltoken optTagId, ltokenList enums )

Definition at line 1755 of file abstract.c. { enumSpecNode n = (enumSpecNode) dmalloc (sizeof (*n)); tagInfo ti; smemberInfo *top = smemberInfo_undefined; n->tok = t; n->opttagid = ltoken_copy (optTagId); n->enums = enums; /* generate sort for this LCL type */ n->sort = sort_makeEnum (optTagId); if (!ltoken_isUndefined (optTagId)) { /* First, check to see if tag is already defined */ ti = symtable_tagInfo (g_symtab, ltoken_getText (optTagId)); if (tagInfo_exists (ti)) { if (ti->kind == TAG_ENUM) { /* 23 Sep 1995 --- had been noting here...is this right? */ ti->content.enums = enums; ti->sort = n->sort; ti->imported = context_inImport (); } else { lclerror (optTagId, message ("Tag %s previously defined as %q, redefined as enum", ltoken_getRawString (optTagId), tagKind_unparse (ti->kind))); /* evs --- shouldn't they be in different name spaces? */ } ltoken_free (optTagId); } else { ti = (tagInfo) dmalloc (sizeof (*ti)); ti->kind = TAG_ENUM; ti->id = optTagId; ti->content.enums = enums; ti->sort = n->sort; ti->imported = context_inImport (); /* First, store tag info in symbol table */ (void) symtable_enterTag (g_symtab, ti); } } /* check that enumeration constants are unique */ ltokenList_reset (enums); while (!ltokenList_isFinished (enums)) { ltoken c = ltokenList_current (enums); smemberInfo *ei = (smemberInfo *) dmalloc (sizeof (*ei)); ei->name = ltoken_getText (c); ei->next = top; ei->sort = n->sort; top = ei; if (!varInfo_exists (symtable_varInfo (g_symtab, ltoken_getText (c)))) { /* put info into symbol table */ varInfo vi = (varInfo) dmalloc (sizeof (*vi)); vi->id = ltoken_copy (c); vi->kind = VRK_ENUM; vi->sort = n->sort; vi->export = TRUE; (void) symtable_enterVar (g_symtab, vi); varInfo_free (vi); } else { lclerror (c, message ("Enumerated value redeclared: %s", ltoken_getRawString (c))); ltokenList_removeCurrent (enums); } ltokenList_advance (enums); /*@-branchstate@*/ } /*@=branchstate@*/ (void) sort_updateEnum (n->sort, top); return (n); }

enumSpecNode makeEnumSpecNode2 ( ltoken t, ltoken tagid )

Definition at line 1852 of file abstract.c. { /* a reference, not a definition */ enumSpecNode n = (enumSpecNode) dmalloc (sizeof (*n)); tagInfo ti = symtable_tagInfo (g_symtab, ltoken_getText (tagid)); n->tok = t; n->opttagid = tagid; n->enums = ltokenList_new (); if (tagInfo_exists (ti)) { if (ti->kind == TAG_ENUM) { n->sort = ti->sort; } else { n->sort = sort_makeNoSort (); lclerror (tagid, message ("Tag %s defined as %q, used as enum", ltoken_getRawString (tagid), tagKind_unparse (ti->kind))); } } else { n->sort = sort_makeNoSort (); lclerror (t, message ("Undefined type: enum %s", ltoken_getRawString (tagid))); } return (n); }

abstBodyNode makeExposedBodyNode ( ltoken t, lclPredicateNode inv )

Definition at line 3119 of file abstract.c. { abstBodyNode x = (abstBodyNode) dmalloc (sizeof (*x)); x->tok = t; x->typeinv = inv; x->fcns = fcnNodeList_undefined; return (x); }

exposedNode makeExposedNode ( ltoken t, lclTypeSpecNode s, declaratorInvNodeList d )

Definition at line 2801 of file abstract.c. { exposedNode n = (exposedNode) dmalloc (sizeof (*n)); n->tok = t; n->type = s; n->decls = d; return n; }

typeNode makeExposedTypeNode ( exposedNode x )

Definition at line 1046 of file abstract.c. { typeNode n = (typeNode) dmalloc (sizeof (*n)); n->kind = TK_EXPOSED; n->content.exposed = x; return (n); }

fcnNode makeFcnNode ( qual specQual, lclTypeSpecNode t, declaratorNode d, globalList g, varDeclarationNodeList privateinits, letDeclNodeList lets, lclPredicateNode checks, lclPredicateNode requires, modifyNode m, lclPredicateNode ensures, lclPredicateNode claims )

Definition at line 2939 of file abstract.c. Referenced by fcnNode_fromDeclarator(). { fcnNode x = (fcnNode) dmalloc (sizeof (*x)); if (d->type != (typeExpr)0 && (d->type)->kind != TEXPR_FCN) { lclerror (d->id, cstring_makeLiteral ("Attempt to specify function without parameter list")); d->type = makeFunctionNode (d->type, paramNodeList_new ()); } x->special = specQual; x->typespec = t; x->declarator = d; x->globals = g; x->inits = privateinits; x->lets = lets; x->checks = checks; x->require = requires; x->modify = m; x->ensures = ensures; x->claim = claims; /* extract info to fill in x->name =; x->signature =; */ x->name = ltoken_copy (d->id); return (x); }

varDeclarationNode makeFileSystemNode ( void )

Definition at line 2620 of file abstract.c. { varDeclarationNode n = (varDeclarationNode) dmalloc (sizeof (*n)); n->isSpecial = TRUE; n->sref = sRef_makeSystemState (); /*@-compdef@*/ return n; /*@=compdef@*/ }

strOrUnionNode makeForwardstrOrUnionNode ( ltoken str, suKind k, ltoken tagid )

Definition at line 2036 of file abstract.c. { strOrUnionNode n = (strOrUnionNode) dmalloc (sizeof (*n)); sort sort = sort_makeNoSort (); tagInfo t; /* a reference, not a definition */ n->kind = k; n->tok = str; n->opttagid = tagid; n->structdecls = stDeclNodeList_new (); /* get sort for this LCL type */ t = symtable_tagInfo (g_symtab, ltoken_getText (tagid)); if (tagInfo_exists (t)) { sort = t->sort; if (!(((t->kind == TAG_STRUCT || t->kind == TAG_FWDSTRUCT) && k == SU_STRUCT) || ((t->kind == TAG_UNION || t->kind == TAG_FWDUNION) && k == SU_UNION))) { lclerror (tagid, message ("Tag %s previously defined as %q, used as %q", ltoken_getRawString (tagid), tagKind_unparse (t->kind), cstring_makeLiteral ((k == SU_STRUCT) ? "struct" : "union"))); } } else { /* ** changed from error: 31 Mar 1994 ** ** lclerror (str, message ("Undefined type: %s %s", s, ltoken_getRawString (tagid)); ** */ /* forward struct's and union's are ok... */ if (k == SU_STRUCT) { (void) checkAndEnterTag (TAG_FWDSTRUCT, ltoken_copy (tagid)); lhForwardStruct (tagid); sort = sort_makeStr (tagid); } else { (void) checkAndEnterTag (TAG_FWDUNION, ltoken_copy (tagid)); lhForwardUnion (tagid); sort = sort_makeUnion (tagid); } } n->sort = sort; return (n); }

typeExpr makeFunctionNode ( typeExpr x, paramNodeList p )

Definition at line 2135 of file abstract.c. Referenced by makeFcnNode(). { typeExpr y = (typeExpr) dmalloc (sizeof (*y)); y->wrapped = 0; y->kind = TEXPR_FCN; y->content.function.returntype = x; y->content.function.args = p; y->sort = sort_makeNoSort (); return (y); }

termNode makeIfTermNode ( ltoken ift, termNode ifn, ltoken thent, termNode thenn, ltoken elset, termNode elsen )

Definition at line 3590 of file abstract.c. { termNode t = (termNode) dmalloc (sizeof (*t)); opFormNode opform = makeOpFormNode (ift, OPF_IF, opFormUnion_createMiddle (0), ltoken_undefined); nameNode nn = makeNameNodeForm (opform); termNodeList args = termNodeList_new (); t->error_reported = FALSE; t->wrapped = 0; termNodeList_addh (args, ifn); termNodeList_addh (args, thenn); termNodeList_addh (args, elsen); t->name = nn; t->args = args; t->kind = TRM_APPLICATION; t->sort = sort_makeNoSort (); t->given = t->sort; t->possibleSorts = sortSet_new (); t->possibleOps = lslOpSet_new (); ltoken_free (thent); ltoken_free (elset); return (t); }

termNode makeInfixTermNode ( termNode x, ltoken op, termNode y )

Definition at line 3644 of file abstract.c. { termNode t = (termNode) dmalloc (sizeof (*t)); opFormNode opform; nameNode nn; termNodeList args = termNodeList_new (); checkAssociativity (x, op); opform = makeOpFormNode (op, OPF_MANYOPM, opFormUnion_createAnyOp (op), ltoken_undefined); nn = makeNameNodeForm (opform); t->error_reported = FALSE; t->wrapped = 0; termNodeList_addh (args, x); termNodeList_addh (args, y); t->name = nn; t->args = args; t->kind = TRM_APPLICATION; t->sort = sort_makeNoSort (); t->given = t->sort; t->possibleSorts = sortSet_new (); /* sort_equal */ t->possibleOps = lslOpSet_new (); return (t); }

initDeclNode makeInitDeclNode ( declaratorNode d, termNode x )

Definition at line 2734 of file abstract.c. { initDeclNode n = (initDeclNode) dmalloc (sizeof (*n)); n->declarator = d; n->value = x; return n; }

interfaceNode makeInterfaceNodeImports ( importNodeList x )

Definition at line 304 of file abstract.c. { interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); lsymbol importSymbol; i->kind = INF_IMPORTS; i->content.imports = x; /* an importNodeList */ importNodeList_elements (x, imp) { importSymbol = ltoken_getRawText (imp->val); if (lsymbolSet_member (g_currentImports, importSymbol)) { lclerror (imp->val, message ("Circular imports: %s", cstring_fromChars (lsymbol_toChars (importSymbol)))); } else { processImport (importSymbol, imp->val, imp->kind); } } end_importNodeList_elements; lhOutLine (cstring_undefined); return (i); }

interfaceNode makeInterfaceNodeUses ( traitRefNodeList x )

Definition at line 333 of file abstract.c. { interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); i->kind = INF_USES; i->content.uses = x; /* read in LSL traits */ return (i); }

varDeclarationNode makeInternalStateNode ( void )

Definition at line 2610 of file abstract.c. { varDeclarationNode n = (varDeclarationNode) dmalloc (sizeof (*n)); n->isSpecial = TRUE; n->sref = sRef_makeInternalState (); /*@-compdef@*/ return n; /*@=compdef@*/ }

lclPredicateNode makeIntraClaimNode ( ltoken t, lclPredicateNode n )

Definition at line 2998 of file abstract.c. { ltoken_free (n->tok); n->tok = t; n->kind = LPD_INTRACLAIM; return (n); }

iterNode makeIterNode ( ltoken id, paramNodeList p )

Definition at line 2910 of file abstract.c. { iterNode x = (iterNode) dmalloc (sizeof (*x)); bool hasYield = FALSE; x->name = id; x->params = p; /* check there is at least one yield param */ paramNodeList_elements (p, pe) { if (paramNode_isYield (pe)) { hasYield = TRUE; break; } } end_paramNodeList_elements if (!hasYield) { lclerror (id, message ("Iterator has no yield parameters: %s", ltoken_getRawString (id))); } return (x); }

lclPredicateNode makeLclPredicateNode ( ltoken t, termNode n, lclPredicateKind k )

Definition at line 3034 of file abstract.c. { lclPredicateNode x = (lclPredicateNode) dmalloc (sizeof (*x)); x->tok = t; x->predicate = n; x->kind = k; return (x); }

lclTypeSpecNode makeLclTypeSpecNodeConj ( lclTypeSpecNode a, lclTypeSpecNode b )

Definition at line 1672 of file abstract.c. Referenced by lclTypeSpecNode_copy(). { lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n)); n->kind = LTS_CONJ; n->pointers = 0; n->quals = qualList_new (); n->content.conj = (lclconj) dmalloc (sizeof (*n->content.conj)); n->content.conj->a = a; n->content.conj->b = b; return (n); }

lclTypeSpecNode makeLclTypeSpecNodeEnum ( enumSpecNode x )

Definition at line 1711 of file abstract.c. Referenced by lclTypeSpecNode_copy(). { lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n)); n->quals = qualList_new (); n->kind = LTS_ENUM; n->pointers = 0; n->content.enumspec = x; return (n); }

lclTypeSpecNode makeLclTypeSpecNodeSU ( strOrUnionNode x )

Definition at line 1699 of file abstract.c. Referenced by lclTypeSpecNode_copy(). { lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n)); n->kind = LTS_STRUCTUNION; n->pointers = 0; n->content.structorunion = x; n->quals = qualList_new (); return (n); }

lclTypeSpecNode makeLclTypeSpecNodeType ( CTypesNode x )

Definition at line 1687 of file abstract.c. Referenced by lclTypeSpecNode_copy(). { lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n)); n->kind = LTS_TYPE; n->pointers = 0; n->content.type = x; n->quals = qualList_new (); return (n); }

letDeclNode makeLetDeclNode ( ltoken varid, lclTypeSpecNode t, termNode term )

Definition at line 964 of file abstract.c. { letDeclNode x = (letDeclNode) dmalloc (sizeof (*x)); varInfo vi = (varInfo) dmalloc (sizeof (*vi)); ltoken errtok; sort s, termsort; if (t != (lclTypeSpecNode) 0) { /* check varid has the same sort as term */ s = lclTypeSpecNode2sort (t); termsort = term->sort; /* should keep the arguments in order */ if (!sort_member_modulo_cstring (s, term) && !term->error_reported) { errtok = termNode_errorToken (term); /* errorShowPoint (tsource_thisLine (lclsource), ltoken_getCol (errtok)); */ /* sprintf (ERRMSG, "expect `%s' type but given term has `%s' type", sort_unparse (s), sort_unparse (termsort)); */ lclerror (errtok, message ("Let declaration expects type %q", sort_unparse (s))); /* evs --- don't know how to generated this message or what it means? */ } } else { s = term->sort; } /* assign variable its type and sort, store in symbol table */ vi->id = ltoken_copy (varid); vi->kind = VRK_LET; vi->sort = s; vi->export = TRUE; (void) symtable_enterVar (g_symtab, vi); varInfo_free (vi); x->varid = varid; x->sortspec = t; x->term = term; x->sort = sort_makeNoSort (); return (x); }

termNode makeLiteralTermNode ( ltoken tok, sort s )

Definition at line 4171 of file abstract.c. { nameNode nn = makeNameNodeId (ltoken_copy (tok)); opInfo oi = symtable_opInfo (g_symtab, nn); lslOp op = (lslOp) dmalloc (sizeof (*op)); termNode n = (termNode) dmalloc (sizeof (*n)); sigNode sign; ltoken range; n->name = nn; n->error_reported = FALSE; n->wrapped = 0; n->kind = TRM_LITERAL; n->literal = tok; n->given = sort_makeNoSort (); n->sort = n->given; n->args = termNodeList_new (); n->possibleSorts = sortSet_new (); n->possibleOps = lslOpSet_new (); /* look up signatures for this operator too */ range = ltoken_create (simpleId, sort_getLsymbol (s)); sign = makesigNode (ltoken_undefined, ltokenList_new (), ltoken_copy (range)); if (opInfo_exists (oi) && (oi->name->isOpId) && (sigNodeSet_size (oi->signatures) > 0)) { sigNodeSet_elements (oi->signatures, x) { if (ltokenList_empty (x->domain)) { lslOp opn = (lslOp) dmalloc (sizeof (*opn)); sort sort; opn->name = nameNode_copy (nn); opn->signature = x; sort = sigNode_rangeSort (x); (void) sortSet_insert (n->possibleSorts, sort); (void) lslOpSet_insert (n->possibleOps, opn); } } end_sigNodeSet_elements; } /* insert into literal term */ (void) sortSet_insert (n->possibleSorts, s); op->name = nameNode_copy (nn); op->signature = sign; (void) lslOpSet_insert (n->possibleOps, op); /* enter the literal as an operator into the operator table */ /* 8/9/93. C's char constant 'c' syntax conflicts with LSL's lslinit.lsi table. Throw out, because it's not needed anyway. */ /* symtable_enterOp (g_symtab, nn, sign); */ if (s == sort_int) { sigNode osign; lslOp opn = (lslOp) dmalloc (sizeof (*opn)); /* if it is a C int, we should overload it as double too because C allows you to say "x > 2". */ (void) sortSet_insert (n->possibleSorts, sort_double); ltoken_setText (range, lsymbol_fromChars ("double")); osign = makesigNode (ltoken_undefined, ltokenList_new (), range); opn->name = nameNode_copy (nn); opn->signature = osign; (void) lslOpSet_insert (n->possibleOps, opn); symtable_enterOp (g_symtab, nameNode_copySafe (nn), sigNode_copy (osign)); } else { ltoken_free (range); } /* future: could overload cstrings to be both char_Vec as well as char_ObjPtr */ /*@-mustfree@*/ return n; }

termNode makeMapTermNode ( termNode pri, ltoken map, ltoken id )

Definition at line 4148 of file abstract.c. { termNode t = (termNode) dmalloc (sizeof (*t)); opFormNode opform = makeOpFormNode (map, OPF_MMAP, opFormUnion_createAnyOp (id), ltoken_undefined); nameNode nn = makeNameNodeForm (opform); termNodeList args = termNodeList_new (); t->error_reported = FALSE; t->wrapped = 0; t->kind = TRM_APPLICATION; t->name = nn; termNodeList_addh (args, pri); t->args = args; t->kind = TRM_APPLICATION; t->sort = sort_makeNoSort (); t->given = t->sort; t->possibleSorts = sortSet_new (); t->possibleOps = lslOpSet_new (); return t; }

termNode makeMatchedNode ( ltoken open, termNodeList args, ltoken close )

Definition at line 4012 of file abstract.c. { /* matched : open args close */ termNode t = (termNode) dmalloc (sizeof (*t)); int size; opFormNode opform; nameNode nn; t->error_reported = FALSE; t->wrapped = 0; size = termNodeList_size (args); opform = makeOpFormNode (open, OPF_MIDDLE, opFormUnion_createMiddle (size), close); nn = makeNameNodeForm (opform); t->name = nn; t->kind = TRM_APPLICATION; t->args = args; t->sort = sort_makeNoSort (); t->given = t->sort; t->possibleSorts = sortSet_new (); t->possibleOps = lslOpSet_new (); /* do sort checking later, not here, incomplete parse */ return (t); }

modifyNode makeModifyNodeRef ( ltoken t, storeRefNodeList y )

Definition at line 779 of file abstract.c. { modifyNode x = (modifyNode) dmalloc (sizeof (*x)); sort sort; x->tok = t; x->hasStoreRefList = TRUE; x->modifiesNothing = FALSE; x->list = y; /* check that all storeRef's are modifiable */ storeRefNodeList_elements (y, sr) { if (storeRefNode_isTerm (sr)) { sort = sr->content.term->sort; if (!sort_mutable (sort) && sort_isValidSort (sort)) { ltoken errtok = termNode_errorToken (sr->content.term); lclerror (errtok, message ("Term denoting immutable object used in modifies list: %q", termNode_unparse (sr->content.term))); } } else { if (!storeRefNode_isSpecial (sr)) { sort = lclTypeSpecNode2sort (sr->content.type); if (storeRefNode_isObj (sr)) { sort = sort_makeObj (sort); } if (!sort_mutable (sort)) { ltoken errtok = lclTypeSpecNode_errorToken (sr->content.type); lclerror (errtok, message ("Immutable type used in modifies list: %q", sort_unparse (sort))); } } } } end_storeRefNodeList_elements; return (x); }

modifyNode makeModifyNodeSpecial ( ltoken t, bool modifiesNothing )

Definition at line 768 of file abstract.c. { modifyNode x = (modifyNode) dmalloc (sizeof (*x)); x->tok = t; x->modifiesNothing = modifiesNothing; x->hasStoreRefList = FALSE; return (x); }

nameNode makeNameNodeForm ( opFormNode opform )

Definition at line 1309 of file abstract.c. Referenced by abstract_init(), makeIfTermNode(), makeInfixTermNode(), makeMapTermNode(), makeMatchedNode(), makePostfixTermNode2(), makePrefixTermNode(), makeSelectTermNode(), makeSqBracketedNode(), nameNode_copySafe(), pushInfixOpPartNode(), and sort_init(). { nameNode nn = (nameNode) dmalloc (sizeof (*nn)); nn->isOpId = FALSE; nn->content.opform = opform; return (nn); }

nameNode makeNameNodeId ( ltoken opid )

Definition at line 1320 of file abstract.c. Referenced by makeLiteralTermNode(), makeOpCallTermNode(), makeSimpleTermNode(), and nameNode_copySafe(). { nameNode nn = (nameNode) dmalloc (sizeof (*nn)); /* ** current LSL -syms output bug produces "if_then_else_" rather ** than 6 separate tokens */ if (ltoken_getText (opid) == ConditionalSymbol) { opFormNode opform = makeOpFormNode (ltoken_undefined, OPF_IF, opFormUnion_createMiddle (0), ltoken_undefined); nn->isOpId = FALSE; nn->content.opform = opform; ltoken_free (opid); } else { nn->isOpId = TRUE; nn->content.opid = opid; } return (nn); }

termNode makeOpCallTermNode ( ltoken op, ltoken open, termNodeList args, ltoken close )

Definition at line 3787 of file abstract.c. { /* like prefixTerm, but with opId LPAR termNodeList RPAR */ termNode t = (termNode) dmalloc (sizeof (*t)); nameNode nn = makeNameNodeId (op); t->error_reported = FALSE; t->wrapped = 0; t->name = nn; t->args = args; t->kind = TRM_APPLICATION; t->sort = sort_makeNoSort (); t->given = t->sort; t->possibleSorts = sortSet_new (); t->possibleOps = lslOpSet_new (); ltoken_free (open); ltoken_free (close); return t; }

opFormNode makeOpFormNode ( ltoken t, opFormKind k, opFormUnion u, ltoken close )

Definition at line 1473 of file abstract.c. Referenced by abstract_init(), makeIfTermNode(), makeInfixTermNode(), makeMapTermNode(), makeMatchedNode(), makeNameNodeId(), makePostfixTermNode2(), makePrefixTermNode(), makeSelectTermNode(), makeSqBracketedNode(), pushInfixOpPartNode(), and sort_init(). { opFormNode n = (opFormNode) dmalloc (sizeof (*n)); unsigned int key = 0; /* ** Assign a hash key here to speed up lookup of operators. */ n->tok = t; n->close = close; n->kind = k; switch (k) { case OPF_IF: n->content.middle = 0; /* OPF_IF is the first enum, so it's 0 */ key = MASH /*@+enumint@*/ (k, k + 1) /*@=enumint@*/; break; case OPF_ANYOP: case OPF_MANYOP: case OPF_ANYOPM: case OPF_MANYOPM: { /* treat eq and = the same */ lsymbol sym = ltoken_getText (u.anyop); if (sym == equalSymbol) { key = MASH (k, eqSymbol); } else { key = MASH (k, ltoken_getText (u.anyop)); } n->content = u; break; } case OPF_MIDDLE: case OPF_MMIDDLE: case OPF_MIDDLEM: case OPF_MMIDDLEM: case OPF_BMIDDLE: case OPF_BMMIDDLE: case OPF_BMIDDLEM: case OPF_BMMIDDLEM: n->content = u; key = MASH (k, u.middle); key = MASH (key, ltoken_getRawText (t)); break; case OPF_SELECT: case OPF_MAP: case OPF_MSELECT: case OPF_MMAP: key = MASH (k, ltoken_getRawText (u.id)); n->content = u; break; default: { llbug (message ("makeOpFormNode: unknown opFormKind: %d", (int) k)); } } n->key = key; return (n); }

paramNode makeParamNode ( lclTypeSpecNode t, typeExpr d )

Definition at line 3171 of file abstract.c. { paramNode x = (paramNode) dmalloc (sizeof (*x)); paramNode_checkQualifiers (t, d); x->type = t; x->paramdecl = d; x->kind = PNORMAL; /*< forgot this! >*/ return (x); }

typeExpr makePointerNode ( ltoken star, typeExpr x )

Definition at line 2497 of file abstract.c. { if (x != (typeExpr)0 && (x->kind == TEXPR_FCN && (x->wrapped == 0))) { x->content.function.returntype = makePointerNode (star, x->content.function.returntype); return x; } else { typeExpr y = (typeExpr) dmalloc (sizeof (*y)); y->wrapped = 0; y->kind = TEXPR_PTR; y->content.pointer = x; y->sort = sort_makeNoSort (); ltoken_free (star); return y; } }

termNode makePostfixTermNode ( termNode secondary, ltokenList postfixops )

Definition at line 3721 of file abstract.c. { termNode top = secondary; ltokenList_elements (postfixops, op) { top = makePostfixTermNode2 (top, ltoken_copy (op)); /*@i@*/ } end_ltokenList_elements; ltokenList_free (postfixops); return (top); /* dep as only? */ }

termNode makePostfixTermNode2 ( termNode secondary, ltoken postfixop )

Definition at line 3740 of file abstract.c. Referenced by makePostfixTermNode(). { termNode t = (termNode) dmalloc (sizeof (*t)); opFormNode opform = makeOpFormNode (postfixop, OPF_MANYOP, opFormUnion_createAnyOp (postfixop), ltoken_undefined); nameNode nn = makeNameNodeForm (opform); termNodeList args = termNodeList_new (); t->error_reported = FALSE; t->wrapped = 0; termNodeList_addh (args, secondary); t->name = nn; t->args = args; t->kind = TRM_APPLICATION; t->sort = sort_makeNoSort (); t->given = t->sort; t->possibleSorts = sortSet_new (); t->possibleOps = lslOpSet_new (); return t; }

termNode makePrefixTermNode ( ltoken op, termNode arg )

Definition at line 3765 of file abstract.c. { termNode t = (termNode) dmalloc (sizeof (*t)); termNodeList args = termNodeList_new (); opFormNode opform = makeOpFormNode (op, OPF_ANYOPM, opFormUnion_createAnyOp (op), ltoken_undefined); nameNode nn = makeNameNodeForm (opform); t->error_reported = FALSE; t->wrapped = 0; t->name = nn; termNodeList_addh (args, arg); t->args = args; t->kind = TRM_APPLICATION; t->sort = sort_makeNoSort (); t->given = t->sort; t->possibleSorts = sortSet_new (); t->possibleOps = lslOpSet_new (); return t; }

programNode makeProgramNode ( stmtNode x )

Definition at line 1024 of file abstract.c. { programNode n = (programNode) dmalloc (sizeof (*n)); n->wrapped = 0; n->kind = ACT_SELF; n->content.self = x; return (n); }

programNode makeProgramNodeAction ( programNodeList x, actionKind k )

Definition at line 1014 of file abstract.c. { programNode n = (programNode) dmalloc (sizeof (*n)); n->wrapped = 0; n->kind = k; n->content.args = x; return (n); }

termNode makeQuantifiedTermNode ( quantifierNodeList qn, ltoken open, termNode t, ltoken close )

Definition at line 3687 of file abstract.c. { sort sort; termNode n = (termNode) dmalloc (sizeof (*n)); quantifiedTermNode q = (quantifiedTermNode) dmalloc (sizeof (*q)); n->name = NULL; /*> missing this --- detected by lclint <*/ n->error_reported = FALSE; n->wrapped = 0; n->error_reported = FALSE; n->kind = TRM_QUANTIFIER; n->possibleSorts = sortSet_new (); n->possibleOps = lslOpSet_new (); n->kind = TRM_UNCHANGEDALL; n->args = termNodeList_new (); /*< forgot this >*/ termNodeList_free (t->args); t->args = termNodeList_new (); sort = sort_bool; n->sort = sort; (void) sortSet_insert (n->possibleSorts, sort); q->quantifiers = qn; q->open = open; q->close = close; q->body = t; n->quantified = q; return (n); }

quantifierNode makeQuantifierNode ( varNodeList v, ltoken quant )

Definition at line 3046 of file abstract.c. { quantifierNode x = (quantifierNode) dmalloc (sizeof (*x)); x->quant = quant; x->vars = v; x->isForall = cstring_equalLit (ltoken_unparse (quant), "\forall"); return (x); }

renamingNode makeRenamingNode ( typeNameNodeList n, replaceNodeList r )

Definition at line 1204 of file abstract.c. { renamingNode ren = (renamingNode) dmalloc (sizeof (*ren)); if (typeNameNodeList_empty (n)) { ren->is_replace = TRUE; ren->content.replace = r; typeNameNodeList_free (n); } else { nameAndReplaceNode nr = (nameAndReplaceNode) dmalloc (sizeof (*nr)); nr->replacelist = r; nr->namelist = n; ren->is_replace = FALSE; ren->content.name = nr; } return (ren); }

replaceNode makeReplaceNameNode ( ltoken t, typeNameNode tn, nameNode nn )

Definition at line 1245 of file abstract.c. { replaceNode r = (replaceNode) dmalloc (sizeof (*r)); r->tok = t; r->isCType = FALSE; r->typename = tn; r->content.renamesortname.name = nn; r->content.renamesortname.signature = (sigNode)NULL; return (r); }

replaceNode makeReplaceNode ( ltoken t, typeNameNode tn, bool is_ctype, ltoken ct, nameNode nn, sigNode sn )

Definition at line 1259 of file abstract.c. { replaceNode r = (replaceNode) dmalloc (sizeof (*r)); r->tok = t; r->isCType = is_ctype; r->typename = tn; if (is_ctype) { r->content.ctype = ct; sigNode_free (sn); nameNode_free (nn); } else { r->content.renamesortname.name = nn; r->content.renamesortname.signature = sn; ltoken_free (ct); } return (r); }

lclPredicateNode makeRequiresNode ( ltoken t, lclPredicateNode n )

Definition at line 3007 of file abstract.c. { ltoken_free (n->tok); n->tok = t; n->kind = LPD_REQUIRES; return (n); }

termNode makeSelectTermNode ( termNode pri, ltoken select, ltoken id )

Definition at line 4123 of file abstract.c. { termNode t = (termNode) dmalloc (sizeof (*t)); opFormNode opform = makeOpFormNode (select, OPF_MSELECT, opFormUnion_createAnyOp (id), ltoken_undefined); nameNode nn = makeNameNodeForm (opform); termNodeList args = termNodeList_new (); t->error_reported = FALSE; t->wrapped = 0; t->name = nn; t->kind = TRM_APPLICATION; termNodeList_addh (args, pri); t->args = args; t->kind = TRM_APPLICATION; t->sort = sort_makeNoSort (); t->given = t->sort; t->possibleSorts = sortSet_new (); t->possibleOps = lslOpSet_new (); return t; }

termNode makeSimpleTermNode ( ltoken varid )

Definition at line 4038 of file abstract.c. { sort theSort = sort_makeNoSort (); lsymbol sym; opInfo oi; varInfo vi; termNode n = (termNode) dmalloc (sizeof (*n)); n->error_reported = FALSE; n->wrapped = 0; n->name = (nameNode) 0; n->given = theSort; n->args = termNodeList_new (); n->possibleSorts = sortSet_new (); n->possibleOps = lslOpSet_new (); sym = ltoken_getText (varid); /* lookup current scope */ vi = symtable_varInfoInScope (g_symtab, sym); if (varInfo_exists (vi)) { theSort = vi->sort; n->kind = TRM_VAR; n->sort = theSort; n->literal = varid; (void) sortSet_insert (n->possibleSorts, theSort); } else { /* need to handle LCL constants */ vi = symtable_varInfo (g_symtab, sym); if (varInfo_exists (vi) && vi->kind == VRK_CONST) { theSort = vi->sort; n->kind = TRM_CONST; n->sort = theSort; n->literal = varid; (void) sortSet_insert (n->possibleSorts, theSort); } else { /* and LSL operators (true, false, new, nil, etc) */ nameNode nn = makeNameNodeId (ltoken_copy (varid)); oi = symtable_opInfo (g_symtab, nn); if (opInfo_exists (oi) && (oi->name->isOpId) && !sigNodeSet_isEmpty (oi->signatures)) { sigNodeSet_elements (oi->signatures, x) { if (ltokenList_empty (x->domain)) /* yes, it really is empty, not not empty */ { lslOp op = (lslOp) dmalloc (sizeof (*op)); op->name = nameNode_copy (nn); op->signature = x; (void) sortSet_insert (n->possibleSorts, sigNode_rangeSort (x)); (void) lslOpSet_insert (n->possibleOps, op); } } end_sigNodeSet_elements; } nameNode_free (nn); if (sortSet_size (n->possibleSorts) == 0) { lclerror (varid, message ("Unrecognized identifier (constant, variable or operator): %s", ltoken_getRawString (varid))); } n->sort = sort_makeNoSort (); n->literal = varid; n->kind = TRM_ZEROARY; } } return (n); }

termNode makeSizeofTermNode ( ltoken op, lclTypeSpecNode type )

Definition at line 4336 of file abstract.c. { termNode t = (termNode) dmalloc (sizeof (*t)); t->name = NULL; /*< missing this >*/ t->error_reported = FALSE; t->wrapped = 0; t->kind = TRM_SIZEOF; t->sort = sort_int; t->literal = op; t->sizeofField = type; t->given = sort_makeNoSort (); t->possibleSorts = sortSet_new (); t->possibleOps = lslOpSet_new (); t->args = termNodeList_new (); (void) sortSet_insert (t->possibleSorts, t->sort); /* nothing to check */ return (t); }

termNode makeSqBracketedNode ( ltoken lbracket, termNodeList args, ltoken rbracket )

Definition at line 3985 of file abstract.c. { termNode t = (termNode) dmalloc (sizeof (*t)); int size; opFormNode opform; nameNode nn; t->error_reported = FALSE; t->wrapped = 0; size = termNodeList_size (args); opform = makeOpFormNode (lbracket, OPF_BMIDDLE, opFormUnion_createMiddle (size), rbracket); nn = makeNameNodeForm (opform); t->name = nn; t->kind = TRM_APPLICATION; t->args = args; t->sort = sort_makeNoSort (); t->given = t->sort; t->possibleSorts = sortSet_new (); t->possibleOps = lslOpSet_new (); /* do sort checking later, not here, incomplete parse */ return (t); }

stmtNode makeStmtNode ( ltoken varId, ltoken fcnId, termNodeList v )

Definition at line 3153 of file abstract.c. { stmtNode n = (stmtNode) dmalloc (sizeof (*n)); n->lhs = varId; n->operator = fcnId; n->args = v; return (n); }

storeRefNode makeStoreRefNodeInternal ( void )

Definition at line 748 of file abstract.c. { storeRefNode x = (storeRefNode) dmalloc (sizeof (*x)); x->kind = SRN_SPECIAL; x->content.ref = sRef_makeInternalState (); return (x); }

storeRefNode makeStoreRefNodeSystem ( void )

Definition at line 758 of file abstract.c. { storeRefNode x = (storeRefNode) dmalloc (sizeof (*x)); x->kind = SRN_SPECIAL; x->content.ref = sRef_makeSystemState (); return (x); }

storeRefNode makeStoreRefNodeTerm ( termNode t )

Definition at line 728 of file abstract.c. { storeRefNode x = (storeRefNode) dmalloc (sizeof (*x)); x->kind = SRN_TERM; x->content.term = t; return (x); }

storeRefNode makeStoreRefNodeType ( lclTypeSpecNode t, bool isObj )

Definition at line 738 of file abstract.c. { storeRefNode x = (storeRefNode) dmalloc (sizeof (*x)); x->kind = isObj ? SRN_OBJ : SRN_TYPE; x->content.type = t; return (x); }

traitRefNode makeTraitRefNode ( ltokenList fl, renamingNode r )

Definition at line 1141 of file abstract.c. { traitRefNode n = (traitRefNode) dmalloc (sizeof (*n)); n->traitid = fl; n->rename = r; return (n); }

typeExpr makeTypeExpr ( ltoken t )

Definition at line 2170 of file abstract.c. { typeExpr x = (typeExpr) dmalloc (sizeof (*x)); x->wrapped = 0; x->kind = TEXPR_BASE; x->content.base = t; x->sort = sort_makeNoSort (); return (x); }

typeNameNode makeTypeNameNode ( bool isObj, lclTypeSpecNode t, abstDeclaratorNode n )

Definition at line 1622 of file abstract.c. { typeNameNode tn = (typeNameNode) dmalloc (sizeof (*tn)); typeNamePack p = (typeNamePack) dmalloc (sizeof (*p)); tn->isTypeName = TRUE; p->isObj = isObj; p->type = t; p->abst = n; tn->opform = (opFormNode) 0; tn->typename = p; return (tn); }

typeNameNode makeTypeNameNodeOp ( opFormNode n )

Definition at line 1637 of file abstract.c. { typeNameNode t = (typeNameNode) dmalloc (sizeof (*t)); t->typename = (typeNamePack) 0; t->opform = n; t->isTypeName = FALSE; return (t); }

CTypesNode makeTypeSpecifier ( ltoken typedefname )

Definition at line 5080 of file abstract.c. { CTypesNode newnode = (CTypesNode) dmalloc (sizeof (*newnode)); typeInfo ti = symtable_typeInfo (g_symtab, ltoken_getText (typedefname)); newnode->intfield = 0; newnode->ctypes = ltokenList_singleton (ltoken_copy (typedefname)); /* if we see "bool" include bool.h header file */ if (ltoken_getText (typedefname) == lsymbol_bool) { lhIncludeBool (); } if (typeInfo_exists (ti)) { /* must we be concern about whether this type is exported by module? No. Because all typedef's are exported. No hiding supported. */ /* Later, may want to keep types around too */ /* 3/2/93, use underlying sort */ newnode->sort = sort_getUnderlying (ti->basedOn); } else { lclerror (typedefname, message ("Unrecognized type: %s", ltoken_getRawString (typedefname))); /* evs --- Don't know how to get this message */ newnode->sort = sort_makeNoSort (); } ltoken_free (typedefname); return newnode; }

termNode makeUnchangedTermNode1 ( ltoken op, ltoken all )

Definition at line 4260 of file abstract.c. { termNode t = (termNode) dmalloc (sizeof (*t)); t->error_reported = FALSE; t->wrapped = 0; t->kind = TRM_UNCHANGEDALL; t->sort = sort_bool; t->literal = op; t->given = sort_makeNoSort (); t->name = NULL; /*< missing this >*/ t->args = termNodeList_new (); t->possibleSorts = sortSet_new (); t->possibleOps = lslOpSet_new (); (void) sortSet_insert (t->possibleSorts, t->sort); ltoken_free (all); return t; }

termNode makeUnchangedTermNode2 ( ltoken op, storeRefNodeList x )

Definition at line 4282 of file abstract.c. { termNode t = (termNode) dmalloc (sizeof (*t)); ltoken errtok; sort sort; t->name = NULL; /*< missing this >*/ t->error_reported = FALSE; t->wrapped = 0; t->kind = TRM_UNCHANGEDOTHERS; t->sort = sort_bool; t->literal = op; t->unchanged = x; t->given = sort_makeNoSort (); t->possibleSorts = sortSet_new (); t->possibleOps = lslOpSet_new (); t->args = termNodeList_new (); (void) sortSet_insert (t->possibleSorts, t->sort); /* check storeRefNode's are mutable, uses sort of term */ storeRefNodeList_elements (x, sto) { if (storeRefNode_isTerm (sto)) { sort = sto->content.term->sort; if (!sort_mutable (sort)) { errtok = termNode_errorToken (sto->content.term); lclerror (errtok, message ("Term denoting immutable object used in unchanged list: %q", termNode_unparse (sto->content.term))); } } else { if (storeRefNode_isType (sto)) { lclTypeSpecNode type = sto->content.type; sort = lclTypeSpecNode2sort (type); if (!sort_mutable (sort)) { errtok = lclTypeSpecNode_errorToken (type); lclerror (errtok, message ("Immutable type used in unchanged list: %q", sort_unparse (sort))); } } } } end_storeRefNodeList_elements; return t; }

varDeclarationNode makeVarDeclarationNode ( lclTypeSpecNode t, initDeclNodeList x, bool isGlobal, bool isPrivate )

Definition at line 2631 of file abstract.c. { varDeclarationNode n = (varDeclarationNode) dmalloc (sizeof (*n)); sort s, s2, initValueSort; ltoken varid, errtok; termNode initValue; declaratorNode vdnode; n->isSpecial = FALSE; n->qualifier = QLF_NONE; n->isGlobal = isGlobal; n->isPrivate = isPrivate; n->decls = x; s = lclTypeSpecNode2sort (t); /* t is an lclTypeSpec, its sort may not be assigned yet */ initDeclNodeList_elements (x, init) { vdnode = init->declarator; varid = vdnode->id; s2 = typeExpr2ptrSort (s, vdnode->type); initValue = init->value; if (termNode_isDefined (initValue) && !initValue->error_reported) { initValueSort = initValue->sort; /* should keep the arguments in order */ if (!sort_member_modulo_cstring (s2, initValue) && !initValue->error_reported) { errtok = termNode_errorToken (initValue); lclerror (errtok, message ("Variable %s declared type %q, initialized to %q", ltoken_unparse (varid), sort_unparse (s2), sort_unparse (initValueSort))); } } /* ** If global, check that it has been declared already, don't push ** onto symbol table yet (wrong scope, done in enteringFcnScope */ if (isGlobal) { varInfo vi = symtable_varInfo (g_symtab, ltoken_getText (varid)); if (!varInfo_exists (vi)) { lclerror (varid, message ("Undeclared global variable: %s", ltoken_getRawString (varid))); } else { if (vi->kind == VRK_CONST) { lclerror (varid, message ("Constant used in global list: %s", ltoken_getRawString (varid))); } } } else { varInfo vi = (varInfo) dmalloc (sizeof (*vi)); vi->id = ltoken_copy (varid); if (isPrivate) { vi->kind = VRK_PRIVATE; /* check that initValue is not empty */ if (initValue == (termNode) 0) { lclerror (varid, message ("Private variable must have initialization: %s", ltoken_getRawString (varid))); } } else { vi->kind = VRK_VAR; } vi->sort = sort_makeGlobal (s2); vi->export = TRUE; vdnode->isRedecl = symtable_enterVar (g_symtab, vi); varInfo_free (vi); } } end_initDeclNodeList_elements; n->type = t; return n; }

varNode makeVarNode ( ltoken varid, bool isObj, lclTypeSpecNode t )

Definition at line 3068 of file abstract.c. { varNode x = (varNode) dmalloc (sizeof (*x)); varInfo vi = (varInfo) dmalloc (sizeof (*vi)); sort sort; vi->id = ltoken_copy (varid); sort = lclTypeSpecNode2sort (t); /* 9/3/93, The following is needed because we want value sorts to be the default, object sort is generated only if there is "obj" qualifier. There are 2 cases: (1) for immutable types (including C primitive types), we need to generate the object sort if qualifier is present; (2) for array, struct and union types, they are already in their object sorts. */ sort = sort_makeVal (sort); /* both cases are now value sorts */ if (isObj) { sort = sort_makeObj (sort); } vi->sort = sort; vi->kind = VRK_QUANT; vi->export = TRUE; (void) symtable_enterVar (g_symtab, vi); varInfo_free (vi); x->varid = varid; x->isObj = isObj; x->type = t; x->sort = sort_makeNoSort (); return (x); }

lslOp makelslOpNode ( nameNode name, sigNode s )

Definition at line 4877 of file abstract.c. Referenced by lslOp_copy(). { lslOp x = (lslOp) dmalloc (sizeof (*x)); x->name = name; x->signature = s; /* enter operator info into symtab */ /* if not, they may need to be renamed in LCL imports */ if (g_lslParsingTraits) { if (name != NULL) { symtable_enterOp (g_symtab, nameNode_copySafe (name), sigNode_copy (s)); } } else { /* nameNode_free (name); */ /* YIKES! */ } return x; }

sigNode makesigNode ( ltoken t, ltokenList domain, ltoken range )

!! Definition at line 1365 of file abstract.c. Referenced by abstract_init(), makeLiteralTermNode(), and sigNode_copy(). { sigNode s = (sigNode) dmalloc (sizeof (*s)); unsigned int key; /* ** Assign a hash key here to speed up lookup of operators. */ s->tok = t; s->domain = domain; s->range = range; key = MASH (0, ltoken_getText (range)); ltokenList_elements (domain, id) { lsymbol sym = ltoken_getText (id); key = MASH (key, sym); } end_ltokenList_elements; s->key = key; return (s); }

stDeclNode makestDeclNode ( lclTypeSpecNode s, declaratorNodeList x )

Definition at line 2124 of file abstract.c. { stDeclNode n = (stDeclNode) dmalloc (sizeof (*n)); n->lcltypespec = s; n->declarators = x; return n; }

strOrUnionNode makestrOrUnionNode ( ltoken str, suKind k, ltoken opttagid, stDeclNodeList x )

Definition at line 1905 of file abstract.c. { strOrUnionNode n = (strOrUnionNode) dmalloc (sizeof (*n)); lsymbolSet set = lsymbolSet_new (); declaratorNodeList declarators; sort fieldsort, tsort1, tsort2; smemberInfo *mi, *top = smemberInfo_undefined; bool doTag = FALSE; bool isStruct = (k == SU_STRUCT); tagInfo t; n->kind = k; n->tok = str; n->opttagid = ltoken_copy (opttagid); n->structdecls = x; n->sort = isStruct ? sort_makeStr (opttagid) : sort_makeUnion (opttagid); if (!ltoken_isUndefined (opttagid)) { /* First, check to see if tag is already defined */ t = symtable_tagInfo (g_symtab, ltoken_getText (opttagid)); if (tagInfo_exists (t)) { if ((t->kind == TAG_FWDUNION && k == SU_UNION) || (t->kind == TAG_FWDSTRUCT && k == SU_STRUCT)) { /* to allow self-recursive types and forward tag declarations */ t->content.decls = stDeclNodeList_copy (x); /* update tag info */ t->sort = n->sort; } else { lclerror (opttagid, message ("Tag %s previously defined as %q, used as %q", ltoken_getRawString (opttagid), tagKind_unparse (t->kind), cstring_makeLiteral (isStruct ? "struct" : "union"))); } } else { doTag = TRUE; } } else { doTag = TRUE; } if (doTag && !ltoken_isUndefined (opttagid)) { t = (tagInfo) dmalloc (sizeof (*t)); /* can either override prev defn or use prev defn */ /* override it so as to detect more errors */ t->kind = (k == SU_STRUCT) ? TAG_STRUCT : TAG_UNION; t->id = opttagid; t->content.decls = stDeclNodeList_copy (x); t->sort = n->sort; t->imported = FALSE; /* Next, update tag info in symbol table */ (void) symtable_enterTagForce (g_symtab, t); } /* check no duplicate field names */ stDeclNodeList_elements (x, i) { fieldsort = lclTypeSpecNode2sort (i->lcltypespec); /* need the locations, not values */ /* fieldsort = sort_makeObj (fieldsort); */ /* 2/19/93, was fieldsort = sort_makeGlobal (fieldsort); */ declarators = i->declarators; declaratorNodeList_elements (declarators, decl) { lsymbol fieldname; mi = (smemberInfo *) dmalloc (sizeof (*mi)); /* need to make dynamic copies */ fieldname = ltoken_getText (decl->id); /* 2/19/93, added */ tsort1 = typeExpr2ptrSort (fieldsort, decl->type); tsort2 = sort_makeGlobal (tsort1); mi->name = fieldname; mi->sort = tsort2; /* fieldsort; */ mi->next = top; top = mi; if (lsymbolSet_member (set, fieldname)) { lclerror (decl->id, message ("Field name reused: %s", ltoken_getRawString (decl->id))); } else { (void) lsymbolSet_insert (set, fieldname); } /*@-branchstate@*/ } end_declaratorNodeList_elements; /*@=branchstate@*/ } end_stDeclNodeList_elements; if (k == SU_STRUCT) { (void) sort_updateStr (n->sort, top); } else { (void) sort_updateUnion (n->sort, top); } /* We shall keep the info with both tags and types if any of them are present. */ lsymbolSet_free (set); return (n); }

paramNode markYieldParamNode ( paramNode p )

Definition at line 5596 of file abstract.c. { p->kind = PYIELD; llassert (p->type != NULL); p->type->quals = qualList_add (p->type->quals, qual_createYield ()); return (p); }

cstring modifyNode_unparse ( modifyNode m )

Definition at line 4794 of file abstract.c. Referenced by fcnNode_unparse(). { if (m != (modifyNode) 0) { if (m->hasStoreRefList) { return (message (" modifies %q; \n", storeRefNodeList_unparse (m->list))); } else { if (m->modifiesNothing) { return (cstring_makeLiteral ("modifies nothing; \n")); } else { return (cstring_makeLiteral ("modifies anything; \n")); } } } return cstring_undefined; }

nameNode nameNode_copy ( nameNode n )

Definition at line 5791 of file abstract.c. Referenced by makeLiteralTermNode(), makeSimpleTermNode(), and symtable_opsWithLegalDomain(). { if (n == NULL) return NULL; return nameNode_copySafe (n); }

nameNode nameNode_copySafe ( nameNode n )

Definition at line 5797 of file abstract.c. Referenced by nameNode_copy(). { if (n->isOpId) { return (makeNameNodeId (ltoken_copy (n->content.opid))); } else { /* error should be detected by lclint: forgot to copy opform! */ return (makeNameNodeForm (opFormNode_copy (n->content.opform))); } }

ltoken nameNode_errorToken ( nameNode nn )

Definition at line 868 of file abstract.c. Referenced by computePossibleSorts(). { if (nn != (nameNode) 0) { if (nn->isOpId) { return nn->content.opid; } else { if (nn->content.opform != NULL) { return nn->content.opform->tok; } } } return ltoken_undefined; }

void nameNode_free ( nameNode n )

Definition at line 5688 of file abstract.c. Referenced by lslOp_free(), makeReplaceNode(), makeSimpleTermNode(), replaceNode_free(), sort_destroyMod(), and symtable_enterOp(). { if (n != NULL) { if (!n->isOpId) { opFormNode_free (n->content.opform); } sfree (n); } }

cstring nameNode_unparse ( nameNode n )

Definition at line 1348 of file abstract.c. Referenced by computePossibleSorts(). { if (n != (nameNode) 0) { if (n->isOpId) { return (cstring_copy (ltoken_getRawString (n->content.opid))); } else { return (opFormNode_unparse (n->content.opform)); } } return cstring_undefined; }

cstring opFormNode_unparse ( opFormNode n )

Definition at line 1561 of file abstract.c. Referenced by nameNode_unparse(), and typeNameNode_unparse(). { if (n != (opFormNode) 0) { switch (n->kind) { case OPF_IF: return (cstring_makeLiteral ("if __ then __ else __ ")); case OPF_ANYOP: return (cstring_copy (ltoken_getRawString (n->content.anyop))); case OPF_MANYOP: return (message ("__ %s", ltoken_getRawString (n->content.anyop))); case OPF_ANYOPM: return (message ("%s __ ", ltoken_getRawString (n->content.anyop))); case OPF_MANYOPM: return (message ("__ %s __ ", ltoken_getRawString (n->content.anyop))); case OPF_MIDDLE: return (message ("%s %q %s", ltoken_getRawString (n->tok), printMiddle (n->content.middle), ltoken_getRawString (n->close))); case OPF_MMIDDLE: return (message ("__ %s %q %s", ltoken_getRawString (n->tok), printMiddle (n->content.middle), ltoken_getRawString (n->close))); case OPF_MIDDLEM: return (message ("%s %q %s __", ltoken_getRawString (n->tok), printMiddle (n->content.middle), ltoken_getRawString (n->close))); case OPF_MMIDDLEM: return (message ("__ %s%q %s __", ltoken_getRawString (n->tok), printMiddle (n->content.middle), ltoken_getRawString (n->close))); case OPF_BMIDDLE: return (message ("[%q]", printMiddle (n->content.middle))); case OPF_BMMIDDLE: return (message ("__ [%q]", printMiddle (n->content.middle))); case OPF_BMIDDLEM: return (message ("[%q] __", printMiddle (n->content.middle))); case OPF_BMMIDDLEM: return (message ("__ [%q] __", printMiddle (n->content.middle))); case OPF_SELECT: return (message (" \\select %s", ltoken_getRawString (n->content.id))); case OPF_MAP: return (message (" \\field_arrow%s", ltoken_getRawString (n->content.id))); case OPF_MSELECT: return (message ("__ \\select %s", ltoken_getRawString (n->content.id))); case OPF_MMAP: return (message ("__ \\field_arrow %s", ltoken_getRawString (n->content.id))); default: llfatalbug (message ("opFormNodeUnparse: unknown kind: %d", (int) n->kind)); } } return cstring_undefined; }

opFormUnion opFormUnion_createAnyOp ( ltoken t )

Definition at line 5577 of file abstract.c. { opFormUnion u; /* do not distinguish between .anyop and .id */ u.anyop = t; return u; }

opFormUnion opFormUnion_createMiddle ( int middle )

Definition at line 5587 of file abstract.c. { opFormUnion u; u.middle = middle; return u; }

void pairNode_free ( pairNode x )

Definition at line 5903 of file abstract.c. Referenced by pairNodeList_free(). { sfree (x); }

paramNode paramNode_copy ( paramNode p )

Definition at line 5908 of file abstract.c. { if (p != NULL) { paramNode ret = (paramNode) dmalloc (sizeof (*ret)); ret->type = lclTypeSpecNode_copy (p->type); ret->paramdecl = typeExpr_copy (p->paramdecl); ret->kind = p->kind; return ret; } return NULL; }

paramNode paramNode_elipsis ( void )

Definition at line 3185 of file abstract.c. { paramNode x = (paramNode) dmalloc (sizeof (*x)); x->type = (lclTypeSpecNode) 0; x->paramdecl = (typeExpr) 0; x->kind = PELIPSIS; return (x); }

void paramNode_free ( paramNode x )

Definition at line 5923 of file abstract.c. Referenced by paramNodeList_free(). { if (x != NULL) { lclTypeSpecNode_free (x->type); typeExpr_free (x->paramdecl); sfree (x); } }

cstring paramNode_unparse ( paramNode x )

Definition at line 3328 of file abstract.c. Referenced by paramNodeList_unparse(). { if (x != (paramNode) 0) { if (x->kind == PELIPSIS) { return (cstring_makeLiteral ("...")); } if (x->paramdecl != (typeExpr) 0) { /* handle (void) */ return (message ("%q %q", lclTypeSpecNode_unparse (x->type), typeExpr_unparse (x->paramdecl))); } else { return (lclTypeSpecNode_unparse (x->type)); } } return cstring_undefined; }

cstring paramNode_unparseComments ( paramNode x )

Definition at line 3566 of file abstract.c. Referenced by paramNodeList_unparseComments(). { if (x != (paramNode) 0) { if (x->kind == PELIPSIS) { return (cstring_makeLiteral ("...")); } if (x->paramdecl != (typeExpr) 0) { /* handle (void) */ return (message ("%q %q", lclTypeSpecNode_unparseComments (x->type), typeExpr_unparseNoBase (x->paramdecl))); } else { return (lclTypeSpecNode_unparseComments (x->type)); } } return cstring_undefined; }

cstring printLeaves2 ( ltokenList f )

Definition at line 1178 of file abstract.c. { return (ltokenList_unparse (f)); }

cstring printRawLeaves2 ( ltokenList f )

Definition at line 1184 of file abstract.c. { bool first = TRUE; cstring s = cstring_undefined; ltokenList_elements (f, i) { if (first) { s = message ("%s", ltoken_getRawString (i)); first = FALSE; } else s = message ("%q, %s", s, ltoken_getRawString (i)); } end_ltokenList_elements; return s; }

cstring privateNode_unparse ( privateNode n )

Definition at line 532 of file abstract.c. { if (n != (privateNode) 0) { switch (n->kind) { case PRIV_CONST: return (constDeclarationNode_unparse (n->content.constdeclaration)); case PRIV_VAR: return (varDeclarationNode_unparse (n->content.vardeclaration)); case PRIV_TYPE: return (typeNode_unparse (n->content.type)); case PRIV_FUNCTION: return (fcnNode_unparse (n->content.fcn)); default: llfatalbug (message ("privateNode_unparse: unknown kind: %d", (int) n->kind)); } } return cstring_undefined; }

void programNode_free ( programNode x )

Definition at line 5933 of file abstract.c. Referenced by programNodeList_free(). { if (x != NULL) { switch (x->kind) { case ACT_SELF: stmtNode_free (x->content.self); break; case ACT_ITER: case ACT_ALTERNATE: case ACT_SEQUENCE: programNodeList_free (x->content.args); break; BADDEFAULT; } sfree (x); } }

cstring programNode_unparse ( programNode p )

Definition at line 4818 of file abstract.c. Referenced by programNodeList_unparse(). { if (p != (programNode) 0) { cstring s = cstring_undefined; int count; switch (p->kind) { case ACT_SELF: { cstring back = cstring_undefined; for (count = p->wrapped; count > 0; count--) { s = cstring_appendChar (s, '('); back = cstring_appendChar (back, ')'); } s = message ("%q%q%q", s, stmtNode_unparse (p->content.self), back); break; } case ACT_ITER: s = message ("*(%q)", programNodeList_unparse (p->content.args)); break; case ACT_ALTERNATE: s = message ("|(%q)", programNodeList_unparse (p->content.args)); break; case ACT_SEQUENCE: s = programNodeList_unparse (p->content.args); break; } return s; } return cstring_undefined; }

termNodeList pushInfixOpPartNode ( termNodeList x, ltoken op, termNode secondary )

Definition at line 3854 of file abstract.c. { termNode lastLeftTerm; termNodeList args = termNodeList_new (); termNode t = (termNode) dmalloc (sizeof (*t)); opFormNode opform; nameNode nn; termNodeList_addh (args, secondary); if (!termNodeList_empty (x)) { termNodeList_reset (x); lastLeftTerm = termNodeList_current (x); checkAssociativity (lastLeftTerm, op); } opform = makeOpFormNode (op, OPF_MANYOPM, opFormUnion_createAnyOp (op), ltoken_undefined); nn = makeNameNodeForm (opform); t->error_reported = FALSE; t->wrapped = 0; t->name = nn; t->kind = TRM_APPLICATION; t->args = args; t->sort = sort_makeNoSort (); t->given = t->sort; t->possibleSorts = sortSet_new (); t->possibleOps = lslOpSet_new (); termNodeList_addh (x, t); /* don't compute sort yet, do it in CollapseInfixTermNode */ return (x); }

quantifierNode quantifierNode_copy ( quantifierNode x )

Definition at line 5949 of file abstract.c. { quantifierNode ret = (quantifierNode) dmalloc (sizeof (*ret)); ret->quant = ltoken_copy (x->quant); ret->vars = varNodeList_copy (x->vars); ret->isForall = x->isForall; return ret; }

void quantifierNode_free ( quantifierNode x )

Definition at line 5960 of file abstract.c. Referenced by quantifierNodeList_free(). { if (x != NULL) { varNodeList_free (x->vars); ltoken_free (x->quant); sfree (x); } }

cstring renamingNode_unparse ( renamingNode x )

Definition at line 1227 of file abstract.c. { if (x != (renamingNode) 0) { if (x->is_replace) { return (replaceNodeList_unparse (x->content.replace)); } else { return (message ("%q%q", typeNameNodeList_unparse (x->content.name->namelist), replaceNodeList_unparse (x->content.name->replacelist))); } } return cstring_undefined; }

void replaceNode_free ( replaceNode x )

Definition at line 5970 of file abstract.c. Referenced by replaceNodeList_free(). { if (x != NULL) { if (x->isCType) { ; } else { nameNode_free (x->content.renamesortname.name); sigNode_free (x->content.renamesortname.signature); } typeNameNode_free (x->typename); ltoken_free (x->tok); sfree (x); } }

cstring replaceNode_unparse ( replaceNode x )

Definition at line 1286 of file abstract.c. Referenced by replaceNodeList_unparse(). { if (x != (replaceNode) 0) { cstring st; st = message ("%q for ", typeNameNode_unparse (x->typename)); if (x->isCType) { st = message ("%q%s", st, ltoken_getRawString (x->content.ctype)); } else { st = message ("%q%q%q", st, nameNode_unparse (x->content.renamesortname.name), sigNode_unparse (x->content.renamesortname.signature)); } return st; } return cstring_undefined; }

void resetImports ( cstring current )

Definition at line 99 of file abstract.c. { lsymbolSet_free (g_currentImports); g_currentImports = lsymbolSet_new (); /* equal_symbol; */ (void) lsymbolSet_insert (g_currentImports, lsymbol_fromChars (cstring_toCharsSafe (current))); }

bool sameNameNode ( nameNode n1, nameNode n2 )

Definition at line 4978 of file abstract.c. Referenced by lslOp_equal(). { if (n1 == n2) return TRUE; if (n1 != (nameNode) 0 && n2 != (nameNode) 0) { if (bool_equal (n1->isOpId, n2->isOpId)) { if (n1->isOpId) return (ltoken_similar (n1->content.opid, n2->content.opid)); else return sameOpFormNode (n1->content.opform, n2->content.opform); } } return FALSE; }

void setExposedType ( lclTypeSpecNode s )

Definition at line 2795 of file abstract.c. { exposedType = s; }

sigNode sigNode_copy ( sigNode s )

Definition at line 5783 of file abstract.c. Referenced by makeLiteralTermNode(), and makelslOpNode(). { llassert (s != NULL); return (makesigNode (ltoken_copy (s->tok), ltokenList_copy (s->domain), ltoken_copy (s->range))); }

sortList sigNode_domain ( sigNode sig )

Definition at line 5555 of file abstract.c. { sortList domain = sortList_new (); if (sig == (sigNode) 0) { ; } else { ltokenList dom = sig->domain; ltokenList_elements (dom, tok) { sortList_addh (domain, sort_fromLsymbol (ltoken_getText (tok))); } end_ltokenList_elements; } return domain; }

bool sigNode_equal ( sigNode n1, sigNode n2 )

Definition at line 5116 of file abstract.c. Referenced by lslOp_equal(). { /* n1 and n2 are never 0 */ return ((n1 == n2) || (n1->key == n2->key && ltoken_similar (n1->range, n2->range) && ltokenList_equal (n1->domain, n2->domain))); }

void sigNode_free ( sigNode x )

Definition at line 5717 of file abstract.c. Referenced by makeReplaceNode(), replaceNode_free(), sigNodeSet_free(), and sigNodeSet_insert(). { if (x != NULL) { ltokenList_free (x->domain); ltoken_free (x->tok); ltoken_free (x->range); sfree (x); } }

void sigNode_markOwned ( sigNode n )

Definition at line 1400 of file abstract.c. Referenced by symtable_enterOp(). { sfreeEventually (n); }

sort sigNode_rangeSort ( sigNode sig )

Definition at line 5542 of file abstract.c. Referenced by computePossibleSorts(), makeLiteralTermNode(), and symtable_opsWithLegalDomain(). { if (sig == (sigNode) 0) { return sort_makeNoSort (); } else { return sort_fromLsymbol (ltoken_getText (sig->range)); } }

cstring sigNode_unparse ( sigNode n )

Definition at line 1389 of file abstract.c. Referenced by replaceNode_unparse(), and sigNodeSet_unparse(). { if (n != (sigNode) 0) { return (message (":%q -> %s", printLeaves2 (n->domain), ltoken_unparse (n->range))); } return cstring_undefined; }

cstring sigNode_unparseText ( sigNode n )

Definition at line 1406 of file abstract.c. Referenced by sigNodeSet_unparseSomeSigs(). { if (n != (sigNode) 0) { return (message ("%q -> %s", printLeaves2 (n->domain), ltoken_unparse (n->range))); } return cstring_undefined; }

void signNode_free ( signNode sn )

Definition at line 5285 of file abstract.c. { sortList_free (sn->domain); ltoken_free (sn->tok); sfree (sn); }

cstring signNode_unparse ( signNode sn )

Definition at line 5293 of file abstract.c. { cstring s = cstring_undefined; if (sn != (signNode) 0) { s = message (": %q -> %s", sortList_unparse (sn->domain), sort_unparseName (sn->range)); } return s; }

stDeclNode stDeclNode_copy ( stDeclNode x )

Definition at line 6033 of file abstract.c. { stDeclNode ret = (stDeclNode) dmalloc (sizeof (*ret)); ret->lcltypespec = lclTypeSpecNode_copySafe (x->lcltypespec); ret->declarators = declaratorNodeList_copy (x->declarators); return ret; }

void stDeclNode_free ( stDeclNode x )

Definition at line 6043 of file abstract.c. Referenced by stDeclNodeList_free(). { if (x != NULL) { lclTypeSpecNode_free (x->lcltypespec); declaratorNodeList_free (x->declarators); sfree (x); } }

cstring stmtNode_unparse ( stmtNode x )

Definition at line 4856 of file abstract.c. { cstring s = cstring_undefined; if (x != (stmtNode) 0) { if (ltoken_isValid (x->lhs)) { s = cstring_concat (ltoken_getRawString (x->lhs), cstring_makeLiteralTemp (" = ")); } s = message ("%q%s (%q)", s, ltoken_getRawString (x->operator), termNodeList_unparse (x->args)); } return s; }

storeRefNode storeRefNode_copy ( storeRefNode x )

Definition at line 5990 of file abstract.c. { storeRefNode ret = (storeRefNode) dmalloc (sizeof (*ret)); ret->kind = x->kind; switch (x->kind) { case SRN_TERM: ret->content.term = termNode_copySafe (x->content.term); break; case SRN_OBJ: case SRN_TYPE: ret->content.type = lclTypeSpecNode_copy (x->content.type); break; case SRN_SPECIAL: ret->content.ref = sRef_copy (x->content.ref); break; } return ret; }

void storeRefNode_free ( storeRefNode x )

Definition at line 6012 of file abstract.c. Referenced by storeRefNodeList_free(). { if (x != NULL) { if (storeRefNode_isTerm (x)) { termNode_free (x->content.term); } else if (storeRefNode_isType (x) || storeRefNode_isObj (x)) { lclTypeSpecNode_free (x->content.type); } else { /* nothing to free */ } sfree (x); } }

cstring strOrUnionNode_unparse ( strOrUnionNode n )

Definition at line 2097 of file abstract.c. Referenced by lclTypeSpecNode_unparse(). { if (n != (strOrUnionNode) 0) { cstring s; switch (n->kind) { case SU_STRUCT: s = cstring_makeLiteral ("struct "); break; case SU_UNION: s = cstring_makeLiteral ("union "); break; BADDEFAULT } if (!ltoken_isUndefined (n->opttagid)) { s = message ("%q%s ", s, ltoken_getRawString (n->opttagid)); } s = message ("%q{%q}", s, stDeclNodeList_unparse (n->structdecls)); return s; } return cstring_undefined; }

cstring taggedUnionNode_unparse ( taggedUnionNode n )

Definition at line 2863 of file abstract.c. Referenced by typeNode_unparse(). { if (n != (taggedUnionNode) 0) { return (message ("tagged union {%q}%q;\n", stDeclNodeList_unparse (n->structdecls), declaratorNode_unparse (n->declarator))); } return cstring_undefined; }

termNode termNode_copySafe ( termNode t )

Definition at line 5820 of file abstract.c. Referenced by storeRefNode_copy(). { termNode ret = termNode_copy (t); llassert (ret != NULL); return ret; }

ltoken termNode_errorToken ( termNode n )

Definition at line 829 of file abstract.c. Referenced by checkSort(), makeConstDeclarationNode(), makeLetDeclNode(), makeModifyNodeRef(), makeUnchangedTermNode2(), and makeVarDeclarationNode(). { if (n != (termNode) 0) { switch (n->kind) { case TRM_LITERAL: case TRM_UNCHANGEDALL: case TRM_UNCHANGEDOTHERS: case TRM_SIZEOF: case TRM_CONST: case TRM_VAR: case TRM_ZEROARY: /* also the default kind, when no in symbol table */ return n->literal; case TRM_QUANTIFIER: return n->quantified->open; case TRM_APPLICATION: if (n->name != NULL) { if (n->name->isOpId) { return n->name->content.opid; } else { llassert (n->name->content.opform != NULL); return n->name->content.opform->tok; } } else { return ltoken_undefined; } } } return ltoken_undefined; }

void termNode_free ( termNode t )

Definition at line 5815 of file abstract.c. Referenced by initDeclNode_free(), letDeclNode_free(), storeRefNode_free(), termNodeList_free(), typeExpr_free(), and updateMatchedNode(). { sfree (t); }

cstring termNode_unparse ( termNode n )

Definition at line 4704 of file abstract.c. Referenced by makeConstDeclarationNode(), termNodeList_unparse(), termNodeList_unparseSecondToCurrent(), termNodeList_unparseTail(), termNodeList_unparseToCurrent(), typeExpr_unparse(), and typeExpr_unparseNoBase(). { cstring s = cstring_undefined; cstring back = cstring_undefined; cstring front = cstring_undefined; int count; if (n != (termNode) 0) { for (count = n->wrapped; count > 0; count--) { front = cstring_appendChar (front, '('); back = cstring_appendChar (back, ')'); } switch (n->kind) { case TRM_LITERAL: case TRM_CONST: case TRM_VAR: case TRM_ZEROARY: s = cstring_copy (ltoken_getRawString (n->literal)); break; case TRM_APPLICATION: { nameNode nn = n->name; if (nn != (nameNode) 0) { if (nn->isOpId) { s = message ("%s (%q) ", ltoken_getRawString (nn->content.opid), termNodeList_unparse (n->args)); /* must we handle n->given ? skip for now */ } else { s = message ("%q ", printTermNode2 (nn->content.opform, n->args, n->given)); } } else { llfatalbug (message ("termNode_unparse: expect non-empty nameNode: TRM_APPLICATION: %q", nameNode_unparse (nn))); } break; } case TRM_UNCHANGEDALL: s = cstring_makeLiteral ("unchanged (all)"); break; case TRM_UNCHANGEDOTHERS: s = message ("unchanged (%q)", storeRefNodeList_unparse (n->unchanged)); break; case TRM_SIZEOF: s = message ("sizeof (%q)", lclTypeSpecNode_unparse (n->sizeofField)); break; case TRM_QUANTIFIER: { quantifiedTermNode x = n->quantified; s = message ("%q%s%q%s", quantifierNodeList_unparse (x->quantifiers), ltoken_getRawString (x->open), termNode_unparse (x->body), ltoken_getRawString (x->close)); break; } } } return (message ("%q%q%q", front, s, back)); }

void traitRefNode_free ( traitRefNode x )

Definition at line 6053 of file abstract.c. Referenced by traitRefNodeList_free(). { if (x != NULL) { ltokenList_free (x->traitid); renamingNode_free (x->rename); sfree (x); } }

sort typeExpr2ptrSort ( sort base, typeExpr t )

Definition at line 5127 of file abstract.c. Referenced by declareForwardType(), enteringClaimScope(), makeConstDeclarationNode(), makeVarDeclarationNode(), and makestrOrUnionNode(). { if (t != (typeExpr) 0) { switch (t->kind) { case TEXPR_BASE: return base; case TEXPR_PTR: return typeExpr2ptrSort (sort_makePtr (ltoken_undefined, base), t->content.pointer); case TEXPR_ARRAY: return typeExpr2ptrSort (sort_makeArr (ltoken_undefined, base), t->content.array.elementtype); case TEXPR_FCN: /* map all hof types to some sort of SRT_HOF */ return sort_makeHOFSort (base); } } return base; }

void typeExpr_free ( typeExpr x )

Definition at line 2322 of file abstract.c. Referenced by declaratorNode_free(), and paramNode_free(). { if (x != (typeExpr) 0) { switch (x->kind) { case TEXPR_BASE: break; case TEXPR_PTR: typeExpr_free (x->content.pointer); break; case TEXPR_ARRAY: typeExpr_free (x->content.array.elementtype); termNode_free (x->content.array.size); break; case TEXPR_FCN: typeExpr_free (x->content.function.returntype); paramNodeList_free (x->content.function.args); break; /*@-branchstate@*/ } /*@=branchstate@*/ sfree (x); } }

cstring typeExpr_name ( typeExpr x )

Definition at line 2471 of file abstract.c. { if (x != (typeExpr) 0) { switch (x->kind) { case TEXPR_BASE: return (cstring_copy (ltoken_getRawString (x->content.base))); case TEXPR_PTR: return (typeExpr_name (x->content.pointer)); case TEXPR_ARRAY: return (typeExpr_name (x->content.array.elementtype)); case TEXPR_FCN: return (typeExpr_name (x->content.function.returntype)); } } /* evs --- 14 Mar 1995 ** not a bug: its okay to have empty parameter names ** llbug ("typeExpr_name: null"); */ return cstring_undefined; }

cstring typeExpr_unparse ( typeExpr x )

Definition at line 2357 of file abstract.c. Referenced by declaratorNode_unparse(), and paramNode_unparse(). { cstring s = cstring_undefined; /* print out types in order of appearance in source */ paramNodeList params; int i; if (x != (typeExpr) 0) { cstring front = cstring_undefined; cstring back = cstring_undefined; llassert (x->wrapped < 100); for (i = x->wrapped; i >= 1; i--) { front = cstring_appendChar (front, '('); back = cstring_appendChar (back, ')'); } switch (x->kind) { case TEXPR_BASE: s = message ("%q%s", s, ltoken_getRawString (x->content.base)); break; case TEXPR_PTR: s = message ("%q*%q", s, typeExpr_unparse (x->content.pointer)); break; case TEXPR_ARRAY: s = message ("%q%q[%q]", s, typeExpr_unparse (x->content.array.elementtype), termNode_unparse (x->content.array.size)); break; case TEXPR_FCN: s = message ("%q%q (", s, typeExpr_unparse (x->content.function.returntype)); params = x->content.function.args; if (!paramNodeList_empty (params)) { s = message ("%q%q", s, paramNodeList_unparse (x->content.function.args)); } s = message ("%q)", s); break; } s = message ("%q%q%q", front, s, back); } else { s = cstring_makeLiteral ("?"); } return s; }

cstring typeExpr_unparseNoBase ( typeExpr x )

Definition at line 2414 of file abstract.c. Referenced by paramNode_unparseComments(). { cstring s = cstring_undefined; /* print out types in order of appearance in source */ paramNodeList params; int i; if (x != (typeExpr) 0) { cstring front = cstring_undefined; cstring back = cstring_undefined; llassert (x->wrapped < 100); for (i = x->wrapped; i >= 1; i--) { front = cstring_appendChar (front, '('); back = cstring_appendChar (back, ')'); } switch (x->kind) { case TEXPR_BASE: s = message ("%q /* %s */", s, ltoken_getRawString (x->content.base)); break; case TEXPR_PTR: s = message ("%q*%q", s, typeExpr_unparseNoBase (x->content.pointer)); break; case TEXPR_ARRAY: s = message ("%q%q[%q]", s, typeExpr_unparseNoBase (x->content.array.elementtype), termNode_unparse (x->content.array.size)); break; case TEXPR_FCN: s = message ("%q%q (", s, typeExpr_unparseNoBase (x->content.function.returntype)); params = x->content.function.args; if (!paramNodeList_empty (params)) { s = message ("%q%q", s, paramNodeList_unparse (x->content.function.args)); } s = message ("%q)", s); break; } s = message ("%q%q%q", front, s, back); } else { s = cstring_makeLiteral ("?"); } return s; }

void typeNameNode_free ( typeNameNode n )

Definition at line 6063 of file abstract.c. Referenced by replaceNode_free(), and typeNameNodeList_free(). { if (n != NULL) { typeNamePack_free (n->typename); opFormNode_free (n->opform); sfree (n); } }

cstring typeNameNode_unparse ( typeNameNode n )

Definition at line 1647 of file abstract.c. Referenced by typeNameNodeList_unparse(). { if (n != (typeNameNode) 0) { if (n->isTypeName) { cstring st = cstring_undefined; typeNamePack p = n->typename; llassert (p != NULL); if (p->isObj) st = cstring_makeLiteral ("obj "); return (message ("%q%q%q", st, lclTypeSpecNode_unparse (p->type), abstDeclaratorNode_unparse (p->abst))); } else return (opFormNode_unparse (n->opform)); } return cstring_undefined; }

cstring typeNode_unparse ( typeNode t )

Definition at line 696 of file abstract.c. Referenced by privateNode_unparse(). { if (t != (typeNode) 0) { switch (t->kind) { case TK_ABSTRACT: return (abstractNode_unparse (t->content.abstract)); case TK_EXPOSED: return (exposedNode_unparse (t->content.exposed)); case TK_UNION: return (taggedUnionNode_unparse (t->content.taggedunion)); default: llfatalbug (message ("typeNode_unparse: unknown kind: %d", (int)t->kind)); } } return cstring_undefined; }

termNode updateMatchedNode ( termNode left, termNode t, termNode right )

Definition at line 3892 of file abstract.c. { opFormNode op; if ((t == (termNode) 0) || (t->name == NULL) || t->name->isOpId) { llbugexitlit ("updateMatchedNode: expect opForm in nameNode"); } op = t->name->content.opform; llassert (op != NULL); if (left == (termNode) 0) { if (right == (termNode) 0) { /* op->kind is not changed */ termNode_free (right); } else { op->kind = OPF_MIDDLEM; op->key = opFormNode2key (op, OPF_MIDDLEM); termNodeList_addh (t->args, right); } } else { termNodeList_addl (t->args, left); if (right == (termNode) 0) { op->kind = OPF_MMIDDLE; op->key = opFormNode2key (op, OPF_MMIDDLE); } else { op->kind = OPF_MMIDDLEM; op->key = opFormNode2key (op, OPF_MMIDDLEM); termNodeList_addh (t->args, right); } } return t; }

termNode updateSqBracketedNode ( termNode left, termNode t, termNode right )

Definition at line 3938 of file abstract.c. { opFormNode op; if ((t == (termNode) 0) || (t->name == NULL) || (t->name->isOpId)) { llbugexitlit ("updateSqBracketededNode: expect opForm in nameNode"); } op = t->name->content.opform; llassert (op != NULL); if (left == (termNode) 0) { if (right == (termNode) 0) { /* op->kind is not changed */ } else { op->kind = OPF_BMIDDLEM; op->key = opFormNode2key (op, OPF_BMIDDLEM); termNodeList_addh (t->args, right); } } else { termNodeList_addl (t->args, left); if (right == (termNode) 0) { op->kind = OPF_BMMIDDLE; op->key = opFormNode2key (op, OPF_BMMIDDLE); } else { op->kind = OPF_BMMIDDLEM; op->key = opFormNode2key (op, OPF_BMMIDDLEM); termNodeList_addh (t->args, right); } } return t; }

void varDeclarationNode_free ( varDeclarationNode x )

Definition at line 6073 of file abstract.c. Referenced by varDeclarationNodeList_free(). { if (x != NULL) { if (x->isSpecial) { ; } else { lclTypeSpecNode_free (x->type); initDeclNodeList_free (x->decls); sfree (x); } } }

cstring varDeclarationNode_unparse ( varDeclarationNode x )

Definition at line 660 of file abstract.c. Referenced by exportNode_unparse(), and privateNode_unparse(). { if (x != (varDeclarationNode) 0) { cstring st; if (x->isSpecial) { return (sRef_unparse (x->sref)); } else { switch (x->qualifier) { case QLF_NONE: st = cstring_undefined; break; case QLF_CONST: st = cstring_makeLiteral ("const "); break; case QLF_VOLATILE: st = cstring_makeLiteral ("volatile "); break; BADDEFAULT; } st = message ("%q%q %q", st, lclTypeSpecNode_unparse (x->type), initDeclNodeList_unparse (x->decls)); return (st); } } return cstring_undefined; }

varNode varNode_copy ( varNode x )

Definition at line 6090 of file abstract.c. { varNode ret = (varNode) dmalloc (sizeof (*ret)); ret->varid = ltoken_copy (x->varid); ret->isObj = x->isObj; ret->type = lclTypeSpecNode_copySafe (x->type); ret->sort = x->sort; return ret; }

void varNode_free ( varNode x )

Definition at line 6102 of file abstract.c. Referenced by varNodeList_free(). { if (x != NULL) { lclTypeSpecNode_free (x->type); ltoken_free (x->varid); sfree (x); } }

---