- Removed more dead code, improved scantags.py
This commit is contained in:
parent
256ec24d87
commit
91b52f6b4a
35
src/dotout.c
35
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?
|
//! Does a term occur in a run?
|
||||||
int
|
int
|
||||||
termOccursInRun (Term t, int run)
|
termOccursInRun (Term t, int run)
|
||||||
|
@ -68,79 +68,6 @@ first_selectable_goal (List bl)
|
|||||||
return 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
|
//! Determine whether a term is an open nonce variable
|
||||||
/**
|
/**
|
||||||
* Does not explore subterms
|
* Does not explore subterms
|
||||||
|
@ -1,6 +1,7 @@
|
|||||||
#!/usr/bin/python
|
#!/usr/bin/python
|
||||||
|
|
||||||
import commands
|
import commands
|
||||||
|
import sys
|
||||||
|
|
||||||
class Tag(object):
|
class Tag(object):
|
||||||
"""
|
"""
|
||||||
@ -9,11 +10,11 @@ class Tag(object):
|
|||||||
|
|
||||||
def __init__(self,tagline):
|
def __init__(self,tagline):
|
||||||
tl = tagline.strip().split('\t')
|
tl = tagline.strip().split('\t')
|
||||||
self.tag = tl[0]
|
self.id = tl[0]
|
||||||
self.filename = tl[1]
|
self.filename = tl[1]
|
||||||
|
|
||||||
def __str__(self):
|
def __str__(self):
|
||||||
return self.tag
|
return self.id
|
||||||
|
|
||||||
class GrepRes(object):
|
class GrepRes(object):
|
||||||
"""
|
"""
|
||||||
@ -63,27 +64,56 @@ def gettags():
|
|||||||
f.close()
|
f.close()
|
||||||
return tags
|
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
|
cmd = "grep \"\\<%s\\>\" *.[chly]" % tag
|
||||||
(reslist,count) = outToRes(commands.getoutput(cmd),[tag.filename])
|
(reslist,count) = outToRes(commands.getoutput(cmd),[tag.filename])
|
||||||
if (len(reslist) == 0) and (count < 2):
|
if (len(reslist) == 0) and (count < 2):
|
||||||
if tag.filename not in filter:
|
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():
|
def main():
|
||||||
# Generate tags
|
# Generate tags
|
||||||
|
print "Generating tags using 'ctags'"
|
||||||
cmd = "ctags *.c *.h *.l *.y"
|
cmd = "ctags *.c *.h *.l *.y"
|
||||||
commands.getoutput(cmd)
|
commands.getoutput(cmd)
|
||||||
|
|
||||||
# Analyze results
|
# Analyze results
|
||||||
|
print "Analyzing results"
|
||||||
filter = ["scanner.c","parser.c"]
|
filter = ["scanner.c","parser.c"]
|
||||||
tags = gettags()
|
tags = gettags()
|
||||||
|
problems = {}
|
||||||
|
total = len(tags)
|
||||||
|
count = 0
|
||||||
|
steps = 20
|
||||||
|
print "_ " * (steps)
|
||||||
|
|
||||||
for t in tags:
|
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()
|
main()
|
||||||
|
|
||||||
|
@ -21,7 +21,6 @@
|
|||||||
const char *progname = "scyther";
|
const char *progname = "scyther";
|
||||||
|
|
||||||
#include "version.h"
|
#include "version.h"
|
||||||
const char *releasetag = SVNVERSION;
|
|
||||||
|
|
||||||
// Structures
|
// Structures
|
||||||
struct switchdata switches;
|
struct switchdata switches;
|
||||||
|
31
src/system.c
31
src/system.c
@ -29,15 +29,6 @@ static int indentState = 0;
|
|||||||
//! Current indent depth.
|
//! Current indent depth.
|
||||||
static int indentDepth = 0;
|
static int indentDepth = 0;
|
||||||
|
|
||||||
//! Allocate memory the size of a run struct.
|
|
||||||
Run
|
|
||||||
makeRun ()
|
|
||||||
{
|
|
||||||
return (Run) malloc (sizeof (struct run));
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
//! Initialise a system structure.
|
//! Initialise a system structure.
|
||||||
/**
|
/**
|
||||||
*@return A system structure pointer with initial values.
|
*@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
|
//! Localize run
|
||||||
/**
|
/**
|
||||||
* Takes a run roledef list and substitutes fromlist into tolist terms.
|
* Takes a run roledef list and substitutes fromlist into tolist terms.
|
||||||
|
18
src/system.h
18
src/system.h
@ -13,7 +13,7 @@
|
|||||||
#define runPointerSet(sys,run,newp) sys->runs[run].index = newp
|
#define runPointerSet(sys,run,newp) sys->runs[run].index = newp
|
||||||
|
|
||||||
enum outputs
|
enum outputs
|
||||||
{ EMPTY, ATTACK, STATESPACE, SCENARIOS, SUMMARY, PROOF };
|
{ EMPTY, ATTACK, STATESPACE, SUMMARY, PROOF };
|
||||||
|
|
||||||
//! Protocol definition.
|
//! Protocol definition.
|
||||||
struct protocol
|
struct protocol
|
||||||
@ -61,20 +61,6 @@ struct run
|
|||||||
//! Shorthand for run pointer.
|
//! Shorthand for run pointer.
|
||||||
typedef struct run *Run;
|
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)
|
//! Structure for information on special terms (cacheing)
|
||||||
struct hiddenterm
|
struct hiddenterm
|
||||||
{
|
{
|
||||||
@ -112,12 +98,10 @@ struct system
|
|||||||
|
|
||||||
/* counters */
|
/* counters */
|
||||||
states_t states; //!< States traversed
|
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 interval; //!< Used to update state printing at certain intervals
|
||||||
states_t claims; //!< Number of claims encountered.
|
states_t claims; //!< Number of claims encountered.
|
||||||
states_t failed; //!< Number of claims failed.
|
states_t failed; //!< Number of claims failed.
|
||||||
int attackid; //!< Global counter of attacks (used for assigning identifiers) within this Scyther call.
|
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_regular_runs; //!< Number of regular runs
|
||||||
int num_intruder_runs; //!< Number of intruder runs
|
int num_intruder_runs; //!< Number of intruder runs
|
||||||
|
|
||||||
|
@ -1481,10 +1481,3 @@ iterateTermOther (const int myrun, Term t, int (*callback) (Term t))
|
|||||||
}
|
}
|
||||||
return term_iterate_deVar (t, testOther, NULL, NULL, NULL);
|
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;
|
|
||||||
}
|
|
||||||
|
23
src/term.h
23
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)
|
#define isTermEqual(t1,t2) isTermEqual2(t1,t2)
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
|
24
src/type.c
24
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.
|
||||||
/**
|
/**
|
||||||
* Check whether a single variable term is instantiated correctly in this
|
* Check whether a single variable term is instantiated correctly in this
|
||||||
|
54
src/xmlout.c
54
src/xmlout.c
@ -111,13 +111,6 @@ xmlOutStates (const char *tag, states_t value)
|
|||||||
eprintf ("</%s>\n", tag);
|
eprintf ("</%s>\n", tag);
|
||||||
}
|
}
|
||||||
|
|
||||||
//! Print a string
|
|
||||||
void
|
|
||||||
xmlOutString (const char *tag, const char *s)
|
|
||||||
{
|
|
||||||
xmlPrint ("<%s>%s</%s>", tag, s, tag);
|
|
||||||
}
|
|
||||||
|
|
||||||
//! Print a term in XML form (iteration inner)
|
//! Print a term in XML form (iteration inner)
|
||||||
void
|
void
|
||||||
xmlTermPrintInner (Term term)
|
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
|
//! Print a term, known to be a role name
|
||||||
/**
|
/**
|
||||||
* Arachne turns all role names into variables for convenience. Here we
|
* Arachne turns all role names into variables for convenience. Here we
|
||||||
@ -294,41 +275,6 @@ xmlRoleTermPrint (const Term t)
|
|||||||
eprintf ("</rolename>\n");
|
eprintf ("</rolename>\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
|
//! Show a term and its type, on single lines
|
||||||
void
|
void
|
||||||
xmlTermType (const Term t)
|
xmlTermType (const Term t)
|
||||||
|
Loading…
Reference in New Issue
Block a user