diff --git a/src/dotout.c b/src/dotout.c index 6ec5373..2e7ba6e 100644 --- a/src/dotout.c +++ b/src/dotout.c @@ -842,41 +842,6 @@ showRanks (const System sys, const int maxrank, const int *ranks, } } -//! Iterate over events (in non-intruder runs) in which some value term occurs first. -// Function should return true for iteration to continue. -int -iterate_first_regular_occurrences (const System sys, - int (*func) (int run, int ev), - const Term t) -{ - int run; - - for (run = 0; run < sys->maxruns; run++) - { - if (sys->runs[run].protocol != INTRUDER) - { - int ev; - Roledef rd; - - rd = sys->runs[run].start; - for (ev = 0; ev < sys->runs[run].step; ev++) - { - if (termSubTerm (rd->from, t) || - termSubTerm (rd->to, t) || termSubTerm (rd->message, t)) - { - // Allright, t occurs here in this run first - if (!func (run, ev)) - { - return false; - } - break; - } - } - } - } - return true; -} - //! Does a term occur in a run? int termOccursInRun (Term t, int run) diff --git a/src/heuristic.c b/src/heuristic.c index e95f547..fb63a7d 100644 --- a/src/heuristic.c +++ b/src/heuristic.c @@ -68,79 +68,6 @@ first_selectable_goal (List bl) return bl; } -//! Give an indication of the amount of consequences binding a term has -/** - * Given a term, returns a float. 0: maximum consequences, 1: no consequences. - */ -float -termBindConsequences (const System sys, Term t) -{ - Termlist openVariables; - - openVariables = termlistAddVariables (NULL, t); - if (openVariables == NULL) - { - // No variables, no consequences - return 1; - } - else - { - // For each run event in the semitrace, check whether it contains any - // of the open variables. - int totalCount; - int affectedCount; - int run; - - totalCount = 0; - affectedCount = 0; - run = 0; - while (run < sys->maxruns) - { - Roledef rd; - int step; - - rd = sys->runs[run].start; - step = 0; - while (step < sys->runs[run].height) - { - Termlist tl; - - tl = openVariables; - while (tl != NULL) - { - if ((rd->type == READ || rd->type == SEND) - && termSubTerm (rd->message, tl->term)) - { - // This run event contains the open variable - affectedCount++; - tl = NULL; - } - else - { - tl = tl->next; - } - } - totalCount++; - step++; - rd = rd->next; - } - run++; - } - - termlistDelete (openVariables); - if (totalCount > 0) - { - // Valid computation - return (float) (totalCount - affectedCount) / totalCount; - } - else - { - // No consequences, ensure no division by 0 - return 1; - } - } -} - //! Determine whether a term is an open nonce variable /** * Does not explore subterms diff --git a/src/scantags.py b/src/scantags.py index 548d1df..0d27c29 100755 --- a/src/scantags.py +++ b/src/scantags.py @@ -1,6 +1,7 @@ #!/usr/bin/python import commands +import sys class Tag(object): """ @@ -9,11 +10,11 @@ class Tag(object): def __init__(self,tagline): tl = tagline.strip().split('\t') - self.tag = tl[0] + self.id = tl[0] self.filename = tl[1] def __str__(self): - return self.tag + return self.id class GrepRes(object): """ @@ -63,27 +64,56 @@ def gettags(): f.close() return tags -def tagoccurs(tag,filter=[]): +def tagoccurs(problems,tag,filter=[]): """ - Check tag occurrences in .c and .h files and show interesting ones. + Check tag occurrences in certain files and show interesting ones. """ cmd = "grep \"\\<%s\\>\" *.[chly]" % tag (reslist,count) = outToRes(commands.getoutput(cmd),[tag.filename]) if (len(reslist) == 0) and (count < 2): if tag.filename not in filter: - print "Possibly used only %i times:\t%s\t%s" % (count,tag.filename,tag) + # this might be a problem, store it + if tag.filename not in problems.keys(): + problems[tag.filename] = {} + problems[tag.filename][tag.id] = count + + return problems + + +def tagreport(problems): + for fn in problems.keys(): + print "file: %s" % fn + for t in problems[fn].keys(): + print "\t%i\t%s" % (problems[fn][t],t) def main(): # Generate tags + print "Generating tags using 'ctags'" cmd = "ctags *.c *.h *.l *.y" commands.getoutput(cmd) # Analyze results + print "Analyzing results" filter = ["scanner.c","parser.c"] tags = gettags() + problems = {} + total = len(tags) + count = 0 + steps = 20 + print "_ " * (steps) + for t in tags: - tagoccurs(t,filter) + problems = tagoccurs(problems,t,filter) + count = count + 1 + if count % (total / steps) == 0: + print "^", + sys.stdout.flush() + print + print + + tagreport (problems) main() + diff --git a/src/switches.c b/src/switches.c index 45934a9..2f10090 100644 --- a/src/switches.c +++ b/src/switches.c @@ -21,7 +21,6 @@ const char *progname = "scyther"; #include "version.h" -const char *releasetag = SVNVERSION; // Structures struct switchdata switches; diff --git a/src/system.c b/src/system.c index cfbf9f4..bff3585 100644 --- a/src/system.c +++ b/src/system.c @@ -29,15 +29,6 @@ static int indentState = 0; //! Current indent depth. static int indentDepth = 0; -//! Allocate memory the size of a run struct. -Run -makeRun () -{ - return (Run) malloc (sizeof (struct run)); -} - - - //! Initialise a system structure. /** *@return A system structure pointer with initial values. @@ -430,28 +421,6 @@ run_prefix_read (const System sys, const int run, Roledef rd, } -//! Create a new local -/** - * Given a term, construct a new local term. Returns NULL if no such term was constructed. - */ -Term -create_new_local (const Term t, const int rid) -{ - if (t != NULL && realTermLeaf (t)) - { - Term newt; - - newt = makeTermType (t->type, TermSymb (t), rid); - newt->stype = t->stype; - - return newt; - } - else - { - return NULL; - } -} - //! Localize run /** * Takes a run roledef list and substitutes fromlist into tolist terms. diff --git a/src/system.h b/src/system.h index 4e9ef7f..e982605 100644 --- a/src/system.h +++ b/src/system.h @@ -13,7 +13,7 @@ #define runPointerSet(sys,run,newp) sys->runs[run].index = newp enum outputs -{ EMPTY, ATTACK, STATESPACE, SCENARIOS, SUMMARY, PROOF }; +{ EMPTY, ATTACK, STATESPACE, SUMMARY, PROOF }; //! Protocol definition. struct protocol @@ -61,20 +61,6 @@ struct run //! Shorthand for run pointer. typedef struct run *Run; -//! Buffer for variables substitution state. -struct varbuf -{ - //! List of closed variables. - Termlist from; - //! List of terms to which the closed variables are bound. - Termlist to; - //! List of open variables. - Termlist empty; -}; - -//! Shorthand for varbuf pointer. -typedef struct varbuf *Varbuf; - //! Structure for information on special terms (cacheing) struct hiddenterm { @@ -112,12 +98,10 @@ struct system /* counters */ states_t states; //!< States traversed - states_t statesScenario; //!< States traversed that are within the scenario, not the prefix states_t interval; //!< Used to update state printing at certain intervals states_t claims; //!< Number of claims encountered. states_t failed; //!< Number of claims failed. int attackid; //!< Global counter of attacks (used for assigning identifiers) within this Scyther call. - int countScenario; //!< Number of scenarios skipped. int num_regular_runs; //!< Number of regular runs int num_intruder_runs; //!< Number of intruder runs diff --git a/src/term.c b/src/term.c index 2984407..8d47b58 100644 --- a/src/term.c +++ b/src/term.c @@ -1481,10 +1481,3 @@ iterateTermOther (const int myrun, Term t, int (*callback) (Term t)) } return term_iterate_deVar (t, testOther, NULL, NULL, NULL); } - -//! Unused function (here for testing of unused function detectors) -int -unusedFunction (int test) -{ - return test + 1; -} diff --git a/src/term.h b/src/term.h index f5776e0..c1a763d 100644 --- a/src/term.h +++ b/src/term.h @@ -142,29 +142,6 @@ int isTermEqualDebug (Term t1, Term t2); ) \ ) -#define isTermEqual3(t1,t2) ((substVar(t1) || substVar(t2)) \ - ? isTermEqualFn(t1,t2) \ - : ( \ - (t1 == t2) \ - ? 1 \ - : ( \ - (t1 == NULL || t2 == NULL || t1->type != t2->type) \ - ? 0 \ - : ( \ - realTermLeaf(t1) \ - ? isTermEqualFn(t1,t2) \ - : ( \ - realTermEncrypt(t2) \ - ? (isTermEqual2(TermKey(t1), TermKey(t2)) && \ - isTermEqual2(TermOp(t1), TermOp(t2))) \ - : (isTermEqual2(TermOp1(t1), TermOp1(t2)) && \ - isTermEqual2(TermOp2(t1), TermOp2(t2))) \ - ) \ - ) \ - ) \ - ) \ - ) - #define isTermEqual(t1,t2) isTermEqual2(t1,t2) #endif diff --git a/src/type.c b/src/type.c index 1e70dfe..c9f1274 100644 --- a/src/type.c +++ b/src/type.c @@ -57,30 +57,6 @@ isTypelistGeneric (const Termlist typelist) } } -//! Check whether a single type constant matches a typelist -/** - * Understands semantics of NULL and TERM_Ticket - */ -int -matchSingleType (Termlist typelist, Term type) -{ - if (typelist == TERMLISTERROR) - { - return 0; - } - else - { - if (isTypelistGeneric (typelist)) - { - return 1; - } - else - { - return inTermlist (typelist, type); - } - } -} - //! Check whether a single variable term is instantiated correctly. /** * Check whether a single variable term is instantiated correctly in this diff --git a/src/xmlout.c b/src/xmlout.c index 5068f2e..b585cda 100644 --- a/src/xmlout.c +++ b/src/xmlout.c @@ -111,13 +111,6 @@ xmlOutStates (const char *tag, states_t value) eprintf ("\n", tag); } -//! Print a string -void -xmlOutString (const char *tag, const char *s) -{ - xmlPrint ("<%s>%s", tag, s, tag); -} - //! Print a term in XML form (iteration inner) void xmlTermPrintInner (Term term) @@ -253,18 +246,6 @@ xmlOutTerm (const char *tag, const Term term) } } -//! Attribute term -void -xmlAttrTerm (const char *tag, const Term term) -{ - if (term != NULL) - { - eprintf (" %s=\"", tag); - xmlTermPrint (term); - eprintf ("\""); - } -} - //! Print a term, known to be a role name /** * Arachne turns all role names into variables for convenience. Here we @@ -294,41 +275,6 @@ xmlRoleTermPrint (const Term t) eprintf ("\n"); } -//! Show a single variable instantiation, depth one -void -xmlVariableDepthOne (const Term variable) -{ - /* - * To print a variable, we would wish to see only the first substitution. - * Therefore, we temporarily undo any further substitutions, and reset - * them at the end. - */ - Term varsubst; // substitution shortcut - Term nextsubst; // temporary buffer - - varsubst = variable->subst; - if (varsubst != NULL && realTermVariable (varsubst)) - { - nextsubst = varsubst->subst; - varsubst->subst = NULL; - } - else - { - nextsubst = NULL; - } - - // Print the actual term - xmlIndentPrint (); - xmlTermPrint (variable); - eprintf ("\n"); - - if (nextsubst != NULL) - { - varsubst->subst = nextsubst; - } - -} - //! Show a term and its type, on single lines void xmlTermType (const Term t)