- Removed some dead code by using scantags.py
This commit is contained in:
parent
1eb1e7849e
commit
256ec24d87
@ -6,7 +6,7 @@
|
|||||||
|
|
||||||
//! Types of exit codes
|
//! Types of exit codes
|
||||||
enum exittypes
|
enum exittypes
|
||||||
{ EXIT_NOATTACK = 0, EXIT_ERROR = 1, EXIT_NOCLAIM = 2, EXIT_ATTACK = 3 };
|
{ EXIT_NOATTACK = 0, EXIT_ERROR = 1, EXIT_ATTACK = 3 };
|
||||||
|
|
||||||
void vprintfstderr (char *fmt, va_list args);
|
void vprintfstderr (char *fmt, va_list args);
|
||||||
void printfstderr (char *fmt, ...);
|
void printfstderr (char *fmt, ...);
|
||||||
|
@ -63,20 +63,27 @@ def gettags():
|
|||||||
f.close()
|
f.close()
|
||||||
return tags
|
return tags
|
||||||
|
|
||||||
def tagoccurs(tag):
|
def tagoccurs(tag,filter=[]):
|
||||||
"""
|
"""
|
||||||
Check tag occurrences in .c and .h files and show interesting ones.
|
Check tag occurrences in .c and .h files and show interesting ones.
|
||||||
"""
|
"""
|
||||||
|
|
||||||
cmd = "grep \"\\<%s\\>\" *.[ch]" % 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):
|
||||||
print "\"%s\" seems to occur only %i times in %s" % (tag,count,tag.filename)
|
if tag.filename not in filter:
|
||||||
|
print "Possibly used only %i times:\t%s\t%s" % (count,tag.filename,tag)
|
||||||
|
|
||||||
|
|
||||||
def main():
|
def main():
|
||||||
|
# Generate tags
|
||||||
|
cmd = "ctags *.c *.h *.l *.y"
|
||||||
|
commands.getoutput(cmd)
|
||||||
|
|
||||||
|
# Analyze results
|
||||||
|
filter = ["scanner.c","parser.c"]
|
||||||
tags = gettags()
|
tags = gettags()
|
||||||
for t in tags:
|
for t in tags:
|
||||||
tagoccurs(t)
|
tagoccurs(t,filter)
|
||||||
|
|
||||||
main()
|
main()
|
||||||
|
83
src/system.c
83
src/system.c
@ -357,89 +357,6 @@ agentOfRun (const System sys, const int run)
|
|||||||
return agentOfRunRole (sys, run, sys->runs[run].role->nameterm);
|
return agentOfRunRole (sys, run, sys->runs[run].role->nameterm);
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
|
||||||
* A new run is created; now we want to know if it depends on any previous run.
|
|
||||||
* This occurs when there is a smaller runid with an identical protocol role, with the
|
|
||||||
* same agent pattern. However, there must be at least a variable in the pattern or no
|
|
||||||
* symmetry gains are to be made.
|
|
||||||
*
|
|
||||||
* Return -1 if there is no such symmetry.
|
|
||||||
*/
|
|
||||||
int
|
|
||||||
staticRunSymmetry (const System sys, const int rid)
|
|
||||||
{
|
|
||||||
int ridSymm; // previous symmetrical run
|
|
||||||
Termlist agents; // list of agents for rid
|
|
||||||
Run runs; // shortcut usage
|
|
||||||
|
|
||||||
ridSymm = -1;
|
|
||||||
runs = sys->runs;
|
|
||||||
agents = runs[rid].rho;
|
|
||||||
while (agents != NULL)
|
|
||||||
{
|
|
||||||
if (isTermVariable (agents->term))
|
|
||||||
ridSymm = rid - 1;
|
|
||||||
agents = agents->next;
|
|
||||||
}
|
|
||||||
/* there is no variable in this roledef, abort */
|
|
||||||
if (ridSymm == -1)
|
|
||||||
return -1;
|
|
||||||
|
|
||||||
agents = runs[rid].rho;
|
|
||||||
while (ridSymm >= 0)
|
|
||||||
{
|
|
||||||
/* compare protocol name, role name */
|
|
||||||
if (runs[ridSymm].protocol == runs[rid].protocol &&
|
|
||||||
runs[ridSymm].role == runs[rid].role)
|
|
||||||
{
|
|
||||||
/* same stuff */
|
|
||||||
int isEqual;
|
|
||||||
Termlist al, alSymm; // agent lists
|
|
||||||
|
|
||||||
isEqual = 1;
|
|
||||||
al = agents;
|
|
||||||
alSymm = runs[ridSymm].rho;
|
|
||||||
while (isEqual && al != NULL)
|
|
||||||
{
|
|
||||||
/* determine equality */
|
|
||||||
if (isTermVariable (al->term))
|
|
||||||
{
|
|
||||||
/* case 1: variable, should match type */
|
|
||||||
if (isTermVariable (alSymm->term))
|
|
||||||
{
|
|
||||||
if (!isTermlistEqual
|
|
||||||
(al->term->stype, alSymm->term->stype))
|
|
||||||
isEqual = 0;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
isEqual = 0;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
/* case 2: constant, should match */
|
|
||||||
if (!isTermEqual (al->term, alSymm->term))
|
|
||||||
isEqual = 0;
|
|
||||||
}
|
|
||||||
alSymm = alSymm->next;
|
|
||||||
al = al->next;
|
|
||||||
}
|
|
||||||
if (al == NULL && isEqual)
|
|
||||||
{
|
|
||||||
/* this candidate is allright */
|
|
||||||
#ifdef DEBUG
|
|
||||||
warning ("Symmetry detection. #%i can depend on #%i.", rid,
|
|
||||||
ridSymm);
|
|
||||||
#endif
|
|
||||||
return ridSymm;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
ridSymm--;
|
|
||||||
}
|
|
||||||
return -1; // signal that no symmetrical run was found
|
|
||||||
}
|
|
||||||
|
|
||||||
//! Determine first read with variables besides agents
|
//! Determine first read with variables besides agents
|
||||||
/**
|
/**
|
||||||
*@todo For now, we assume it is simply the first read after the choose, if there is one.
|
*@todo For now, we assume it is simply the first read after the choose, if there is one.
|
||||||
|
@ -15,9 +15,6 @@
|
|||||||
enum outputs
|
enum outputs
|
||||||
{ EMPTY, ATTACK, STATESPACE, SCENARIOS, SUMMARY, PROOF };
|
{ EMPTY, ATTACK, STATESPACE, SCENARIOS, SUMMARY, PROOF };
|
||||||
|
|
||||||
enum engines
|
|
||||||
{ POR_ENGINE, ARACHNE_ENGINE };
|
|
||||||
|
|
||||||
//! Protocol definition.
|
//! Protocol definition.
|
||||||
struct protocol
|
struct protocol
|
||||||
{
|
{
|
||||||
|
@ -32,10 +32,6 @@ extern int inTermlist (); // suppresses a warning, but at what cost?
|
|||||||
|
|
||||||
void indent (void);
|
void indent (void);
|
||||||
|
|
||||||
/* useful macros */
|
|
||||||
|
|
||||||
//! Undefined run identifier in a term
|
|
||||||
#define RID_UNDEF MIN_INT
|
|
||||||
/* main code */
|
/* main code */
|
||||||
|
|
||||||
/* Two types of terms: general, and normalized. Normalized rewrites all
|
/* Two types of terms: general, and normalized. Normalized rewrites all
|
||||||
|
@ -38,9 +38,7 @@
|
|||||||
#define CALLOC(k,n) (calloc((unsigned)(k),(unsigned)(n)))
|
#define CALLOC(k,n) (calloc((unsigned)(k),(unsigned)(n)))
|
||||||
#define FREE(x) (free((char*)(x)))
|
#define FREE(x) (free((char*)(x)))
|
||||||
#define MALLOC(n) (malloc((unsigned)(n)))
|
#define MALLOC(n) (malloc((unsigned)(n)))
|
||||||
#define NEW(t) ((t*)allocate(sizeof(t)))
|
//#define REALLOC(p,n) (realloc((char*)(p),(unsigned)(n)))
|
||||||
#define NEW2(n,t) ((t*)allocate((unsigned)((n)*sizeof(t))))
|
|
||||||
#define REALLOC(p,n) (realloc((char*)(p),(unsigned)(n)))
|
|
||||||
|
|
||||||
/* actual functions */
|
/* actual functions */
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user