---

checking.c File Reference

#include "lclintMacros.nf"
#include "llbasic.h"
#include "llgrammar.h"
#include "checking.h"
#include "lclscan.h"

Go to the source code of this file.

Functions
termNode	computePossibleSorts ( termNode t)
termNode	checkSort ( termNode t)
void	checkLclPredicate (ltoken t, lclPredicateNode n)

---

Function Documentation

void checkLclPredicate ( ltoken t, lclPredicateNode n )

Definition at line 384 of file checking.c. { sort theSort; if ((n == NULL) || (n->predicate == NULL)) { llcontbuglit ("checkLclPredicate expects valid lclPredicate. " "Skipping current check"); return; } /* check only if there are no previous errors */ if (!n->predicate->error_reported) { /* check that the sort of n is boolean */ theSort = n->predicate->sort; if (!sort_compatible (theSort, sort_capBool)) { if (sort_isNoSort (theSort)) { ; /* "Expects a boolean term. Given term has unknown sort" */ } else { cstring clauset = ltoken_getRawString (t); if (cstring_firstChar (clauset) == '(') { clauset = cstring_makeLiteral ("Equality"); } else { /* uppercase first letter */ clauset = cstring_copy (clauset); cstring_setChar (clauset, 1, (char) toupper (cstring_firstChar (clauset))); } lclerror (t, message ("%q expects a boolean term, given %q.", clauset, sort_unparse (theSort))); } } } }

termNode checkSort ( termNode t )

Definition at line 223 of file checking.c. { sortSet sorts; sort theSort; int size; ltoken errtok; (void) computePossibleSorts (t); sorts = t->possibleSorts; llassert (sortSet_isDefined (sorts)); size = sortSet_size (sorts); switch (size) { case 0: /* complain later */ break; case 1: /* just right */ theSort = sortSet_choose (sorts); assignSorts (t, theSort); break; default: /* we allow C literals to have multiple sorts */ if (t->kind != TRM_LITERAL) { errtok = termNode_errorToken (t); t->error_reported = TRUE; lclerror (errtok, message ("Term %q: can have more than one possible type. Possible types: %q", termNode_unparse (t), sortSet_unparseClean (sorts))); } } return t; }

termNode computePossibleSorts ( termNode t )

Definition at line 49 of file checking.c. Referenced by checkSort(). { ltoken errtok; if (t != (termNode) 0) { switch (t->kind) { case TRM_LITERAL: case TRM_CONST: case TRM_VAR: case TRM_ZEROARY: case TRM_SIZEOF: case TRM_UNCHANGEDALL: case TRM_UNCHANGEDOTHERS: case TRM_QUANTIFIER: break; case TRM_APPLICATION: { bool fail = FALSE; sortSetList argSorts = sortSetList_new (); lslOpSet ops; sortSet standards; if (termNodeList_size (t->args) != 0) { termNodeList_elements (t->args, arg) { (void) computePossibleSorts (arg); if (sortSet_size (arg->possibleSorts) == 0) { fail = TRUE; } else { sortSetList_addh (argSorts, arg->possibleSorts); } } end_termNodeList_elements; if (fail) { lslOpSet_free (t->possibleOps); sortSetList_free (argSorts); t->possibleOps = lslOpSet_new (); return t; } } ops = symtable_opsWithLegalDomain (g_symtab, t->name, argSorts, t->given); lslOpSet_free (t->possibleOps); t->possibleOps = ops; lslOpSet_elements (t->possibleOps, op) { sort sort; sort = sigNode_rangeSort (op->signature); (void) sortSet_insert (t->possibleSorts, sort); } end_lslOpSet_elements; standards = standardOperators (t->name, argSorts, t->given); sortSet_elements (standards, el) { (void) sortSet_insert (t->possibleSorts, el); } end_sortSet_elements; sortSet_free (standards); if (!(t->error_reported) && sortSet_size (t->possibleSorts) == 0) { unsigned int arity = termNodeList_size (t->args); errtok = nameNode_errorToken (t->name); /* errorShowPoint (tsource_thisLine (lclsource), ltoken_getCol (errtok)); */ if (isStandardOperator (t->name)) { lclerror (errtok, message ("Type error: %q not declared for %q", nameNode_unparse (t->name), printBadArgs (argSorts))); } else if (t->name != NULL && symtable_opExistsWithArity (g_symtab, t->name, arity)) { sigNodeSet possibleOps = symtable_possibleOps (g_symtab, t->name); cstring opName = nameNode_unparse (t->name); /* ** all these will be standardOperators soon... */ if (cstring_equalLit (opName, "__ [__]")) { lclerror (errtok, message ("Type error: %q not declared for %q", opName, printBadArgs (argSorts))); } else { lclerror (errtok, message ("Type error: %q declared: %q\ngiven: %q", opName, sigNodeSet_unparseSomeSigs (possibleOps), printBadArgs (argSorts))); } } else { sigNodeSet possibleOps; int npossibleOps; llassert (t->name != NULL); possibleOps = symtable_possibleOps (g_symtab, t->name); npossibleOps = sigNodeSet_size (possibleOps); /* ** evs --- check is it is wrong arity... */ if (npossibleOps == 0) { lclerror (errtok, message ("Undeclared operator: %q", nameNode_unparse (t->name))); } else { lclerror (errtok, message ("Operator %q declared for %q arguments, given %d", nameNode_unparse (t->name), sigNodeSet_unparsePossibleAritys (possibleOps), arity)); } } t->error_reported = TRUE; } sortSetList_free (argSorts); break; } } } return t; }

---