andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Many ansi updates.

Browse Source
This commit is contained in:
ccremers 2004-05-26 12:17:09 +00:00
parent b5ddd75d95
commit ca01a09377
12 changed files with 162 additions and 114 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/knowledge.c
View File

@ -267,6 +267,8 @@ knowledgeSetInverses (Knowledge know, Termlist tl)
int
inKnowledge (const Knowledge know, Term term)
{
mindwipe (know, inKnowledge (know, term));
/* if there is no term, then it's okay 'fur sure' */
if (term == NULL)
return 1;
@ -274,8 +276,6 @@ inKnowledge (const Knowledge know, Term term)
if (know == NULL)
return 0;
mindwipe (know, inKnowledge (know, term));
term = deVar (term);
if (isTermLeaf (term))
{
@ -489,8 +489,6 @@ knowledgeNew (const Knowledge oldk, const Knowledge newk)
{
Termlist newtl;
newtl = NULL;
void addNewStuff (Termlist tl)
{
while (tl != NULL)
@ -502,6 +500,8 @@ knowledgeNew (const Knowledge oldk, const Knowledge newk)
tl = tl->next;
}
}
newtl = NULL;
addNewStuff (newk->basic);
addNewStuff (newk->encrypt);
return newtl;

9
src/latex.c
View File

@ -324,13 +324,14 @@ latexDeclInst (const System sys, int run)
void
latexEventSpace (int amount)
{
int i;
if (pass < 2)
{
/* not printing */
return;
}
int i;
//printf("%% number of newlines: %d\n",amount);
for (i = 0; i < EVENTSPACE * amount; i++)
printf ("\\nextlevel\n");
@ -904,6 +905,9 @@ attackDisplayLatex (System sys)
}
else
{
Termlist protocolnames;
Term pname;
/* slightly stretch measurements */
printf ("\\addtolength{\\maxmscall}{2\\mscspacer}\n");
printf ("\\addtolength{\\maxmscaction}{\\mscspacer}\n");
@ -920,8 +924,7 @@ attackDisplayLatex (System sys)
/* create MSC title, involving protocol names and such. */
Termlist protocolnames = NULL;
Term pname;
protocolnames = NULL;
for (i = 0; i < width; i++)
{
if (runPosition[i] > 0)

22
src/main.c
View File

@ -407,8 +407,12 @@ exit:
void
timersPrint (const System sys)
{
/* display stats, header first */
#define NOTIMERS
/* display stats, header first */
#ifdef NOTIMERS
fprintf (stderr, "States\t\tAttack\n");
#else
fprintf (stderr, "Time\t\tStates\t\tAttack\t\tst/sec\n");
/* print time */
@ -416,6 +420,7 @@ timersPrint (const System sys)
double seconds;
seconds = (double) clock () / CLOCKS_PER_SEC;
fprintf (stderr, "%.3e\t", seconds);
#endif
/* states traversed */
@ -441,13 +446,9 @@ timersPrint (const System sys)
fprintf (stderr, "None\t\t");
}
/*
printf("%.3e (%li) claims encountered.\n",(double)
sys->claims, sys->claims);
printf("%.3e (%li) claims failed.\n",(double)
sys->failed, sys->failed);
*/
#ifdef NOTIMERS
fprintf (stderr, "\n");
#else
/* states per second */
if (seconds > 0)
@ -462,6 +463,7 @@ timersPrint (const System sys)
}
fprintf (stderr, "\n");
#endif
}
//! Analyse the model by incremental runs.
@ -527,6 +529,8 @@ MC_incTraces (const System sys)
int res;
tracestep = 3; /* what is a sensible stepping size? */
flag = 1;
maxtracelen = getMaxTraceLength (sys);
tracelen = maxtracelen - tracestep;
while (tracelen > 6) /* what is a reasonable minimum? */
@ -589,3 +593,5 @@ modelCheck (const System sys)
timersPrint (sys);
return (sys->failed);
}

5
src/match_basic.c
View File

@ -180,6 +180,7 @@ matchRead_basic (const System sys, const int run,
Roledef rd;
int flag = 0;
struct fvpass fp;
Termlist varlist;
int solution (struct fvpass fp, Knowledge know)
{
@ -222,7 +223,7 @@ matchRead_basic (const System sys, const int run,
}
rd = runPointerGet (sys, run);
Termlist varlist = termlistAddVariables (NULL, rd->message);
varlist = termlistAddVariables (NULL, rd->message);
fp.sys = sys;
fp.run = run;
@ -237,8 +238,10 @@ matchRead_basic (const System sys, const int run,
printf ("{\n");
}
#endif
flag = fixVariablelist (fp, sys->know, varlist, rd->message);
termlistDelete (varlist);
#ifdef DEBUG
if (DEBUGL (5))
{

120
src/match_clp.c
View File

@ -105,11 +105,13 @@ solve (const struct solvepass sp, Constraintlist solvecons)
if (tlres != NULL)
{
Constraintlist cl;
copied = 1;
/* sometimes not needed, when no substitutions took place */
oldcl = solvecons;
solvecons = constraintlistDuplicate (solvecons);
Constraintlist cl = solvecons;
cl = solvecons;
while (cl != NULL)
{
cl->constraint->know =
@ -220,6 +222,38 @@ matchRead_clp (const System sys, const int run, int (*proceed) (System, int))
Constraint co;
Roledef runPoint;
int flag;
struct solvepass sp;
/* check solvability */
int solution (const struct solvepass sp, const Constraintlist cl)
{
Knowledge oldknow;
int flag;
int copied;
Constraintlist oldcl;
oldknow = NULL;
flag = 0;
copied = 0;
oldcl = sys->constraints;
sys->constraints = cl;
if (knowledgeSubstNeeded (sys->know))
{
copied = 1;
oldknow = sys->know;
sys->know = knowledgeSubstDo (sys->know);
}
flag = sp.proceed (sys, run);
if (copied)
{
knowledgeDelete (sys->know);
sys->know = oldknow;
knowledgeSubstUndo (sys->know);
}
sys->constraints = oldcl;
return flag;
}
/* save old state */
@ -241,33 +275,6 @@ matchRead_clp (const System sys, const int run, int (*proceed) (System, int))
}
#endif
/* check solvability */
int solution (const struct solvepass sp, const Constraintlist cl)
{
Knowledge oldknow = NULL;
Constraintlist oldcl = sys->constraints;
int flag = 0;
int copied = 0;
sys->constraints = cl;
if (knowledgeSubstNeeded (sys->know))
{
copied = 1;
oldknow = sys->know;
sys->know = knowledgeSubstDo (sys->know);
}
flag = sp.proceed (sys, run);
if (copied)
{
knowledgeDelete (sys->know);
sys->know = oldknow;
knowledgeSubstUndo (sys->know);
}
sys->constraints = oldcl;
return flag;
}
struct solvepass sp;
sp.solution = solution;
sp.sys = sys;
sp.run = run;
@ -300,6 +307,7 @@ secret_clp (const System sys, const Term t)
Constraintlist oldcl, newcl;
Constraint co;
int flag;
struct solvepass sp;
/* save old state */
oldcl = sys->constraints;
@ -312,7 +320,6 @@ secret_clp (const System sys, const Term t)
/* check solvability */
struct solvepass sp;
sp.solution = NULL;
sp.sys = sys;
flag = !solve (sp, sys->constraints);
@ -377,10 +384,13 @@ sendAdd_clp (const System sys, const int run, const Termlist tl)
{
/* difficult case: variable in inverse
* key. We have to branch. */
Knowledge oldknow;
Constraint co;
Constraintlist clold, clbuf;
/* branch 1 : invkey not in knowledge */
/* TODO this yields a negative constraint, which we omit for the time being */
Knowledge oldknow = knowledgeDuplicate (sys->know);
oldknow = knowledgeDuplicate (sys->know);
knowledgeAddTerm (sys->know, t);
sendAdd_clp (sys, run, tl->next);
@ -390,11 +400,11 @@ sendAdd_clp (const System sys, const int run, const Termlist tl)
/* branch 2 : invkey in knowledge */
oldknow = knowledgeDuplicate (sys->know);
Constraintlist clold = sys->constraints;
Constraintlist clbuf = constraintlistShallow (clold);
clold = sys->constraints;
clbuf = constraintlistShallow (clold);
tl2 = termlistShallow (tl->next);
Constraint co = makeConstraint (invkey, sys->know);
co = makeConstraint (invkey, sys->know);
sys->constraints = constraintlistAdd (clbuf, co);
/* we _could_ explore first if this is solveable */
knowledgeAddTerm (sys->know, t);
@ -426,10 +436,12 @@ send_clp (const System sys, const int run)
{
/* new knowledge, must store old state */
Knowledge oldknow;
Termlist tl;
oldknow = sys->know;
sys->know = knowledgeDuplicate (sys->know);
Termlist tl = termlistAdd (NULL, rd->message);
tl = termlistAdd (NULL, rd->message);
sendAdd_clp (sys, run, tl);
termlistDelete (tl);
@ -447,26 +459,20 @@ isPossible_clp (const System sys, const int run, int
Constraint co;
Roledef runPoint;
int flag;
/* save old state */
oldcl = sys->constraints;
newcl = constraintlistShallow (oldcl);
/* creat new state */
runPoint = runPointerGet (sys, run);
/* add the new constraint */
co = makeConstraint (t, k);
newcl = constraintlistAdd (newcl, co);
sys->constraints = newcl;
struct solvepass sp;
/* check solvability */
int solution (const struct solvepass sp, const Constraintlist cl)
{
Knowledge oldknow = NULL;
Constraintlist oldcl = sys->constraints;
int flag = 0;
int copied = 0;
Knowledge oldknow;
Constraintlist oldcl;
int flag;
int copied;
oldknow = NULL;
oldcl = sys->constraints;
flag = 0;
copied = 0;
sys->constraints = cl;
if (knowledgeSubstNeeded (sys->know))
@ -486,7 +492,19 @@ isPossible_clp (const System sys, const int run, int
return flag;
}
struct solvepass sp;
/* save old state */
oldcl = sys->constraints;
newcl = constraintlistShallow (oldcl);
/* creat new state */
runPoint = runPointerGet (sys, run);
/* add the new constraint */
co = makeConstraint (t, k);
newcl = constraintlistAdd (newcl, co);
sys->constraints = newcl;
sp.solution = solution;
sp.sys = sys;
sp.run = run;

70
src/output.c
View File

@ -200,17 +200,32 @@ correspondingSend (System sys, int rd)
void
tracePrint (System sys)
{
int i, j;
int lastrid;
int width;
Termlist newtl;
void sticks (int i)
{
while (i > 0)
{
printf ("|\t");
i--;
}
}
void sticksLine (void)
{
sticks (width);
printf ("\n");
}
if (sys->latex)
{
//latexTracePrint(sys);
return;
}
int i, j;
int lastrid;
int width;
Termlist newtl;
/* fix the 'next' knowledge, this is required because sometimes
* when calling this function, the next knowledge is not stored
* yet, but required for the general form of the output . */
@ -270,21 +285,6 @@ tracePrint (System sys)
/* now we print the actual trace */
void sticks (int i)
{
while (i > 0)
{
printf ("|\t");
i--;
}
}
void sticksLine (void)
{
sticks (width);
printf ("\n");
}
linePrint (width);
lastrid = -1;
for (i = 0; i <= sys->step; i++)
@ -356,6 +356,21 @@ attackDisplayAscii (System sys)
Termlist newtl;
struct tracebuf *tb;
void sticks (int i)
{
while (i > 0)
{
printf ("|\t");
i--;
}
}
void sticksLine (void)
{
sticks (width);
printf ("\n");
}
/* attack trace buffer */
tb = sys->attack;
length = sys->attack->length;
@ -413,21 +428,6 @@ attackDisplayAscii (System sys)
/* now we print the actual trace */
void sticks (int i)
{
while (i > 0)
{
printf ("|\t");
i--;
}
}
void sticksLine (void)
{
sticks (width);
printf ("\n");
}
linePrint (width);
lastrid = -1;
for (i = 0; i < length; i++)

15
src/runs.c
View File

@ -404,9 +404,11 @@ agentOfRun (const System sys, const int run)
Roledef
roledefDuplicate1 (const Roledef rd)
{
Roledef newrd;
if (rd == NULL)
return NULL;
Roledef newrd = makeRoledef ();
newrd = makeRoledef ();
memcpy (newrd, rd, sizeof (struct roledef));
newrd->next = NULL;
return newrd;
@ -419,9 +421,11 @@ roledefDuplicate1 (const Roledef rd)
Roledef
roledefDuplicate (Roledef rd)
{
Roledef newrd;
if (rd == NULL)
return NULL;
Roledef newrd = roledefDuplicate1 (rd);
newrd = roledefDuplicate1 (rd);
newrd->next = roledefDuplicate (rd->next);
return newrd;
}
@ -472,6 +476,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
Termlist fromlist = NULL;
Termlist tolist = NULL;
Term extterm = NULL;
Term newvar;
/* claim runid, allocate space */
rid = sys->maxruns;
@ -493,7 +498,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
{
/* There is a TYPE constant in the parameter list.
* Generate a new local variable for this run, with this type */
Term newvar = makeTermType (VARIABLE, scanfrom->term->left.symb, rid);
newvar = makeTermType (VARIABLE, scanfrom->term->left.symb, rid);
sys->variables = termlistAdd (sys->variables, newvar);
newvar->stype = termlistAdd (NULL, scanto->term);
tolist = termlistAdd (tolist, newvar);
@ -785,6 +790,8 @@ protocolsPrint (Protocol p)
void
rolePrint (Role r)
{
Roledef rd;
if (r == NULL)
return;
@ -794,7 +801,7 @@ rolePrint (Role r)
printf ("]]\n");
locVarPrint (r->locals);
Roledef rd = r->roledef;
rd = r->roledef;
while (rd != NULL)
{
roledefPrint (rd);

4
src/substitutions.c
View File

@ -209,11 +209,13 @@ substitutionlistConcat (Substitutionlist sl1, Substitutionlist sl2)
Termlist
substitutionBatch (Termlist tl, Substitutionlist sl)
{
Termlist newtl;
if (tl == NULL)
return NULL;
if (sl == NULL)
return termlistDuplicate (tl);
Termlist newtl = NULL;
newtl = NULL;
while (tl != NULL)
{
newtl = termlistAdd (newtl, termSubstituteList (tl->term, sl));

11
src/symbols.c
View File

@ -104,10 +104,12 @@ hash (char *s)
void
insert (Symbol s)
{
int hv;
if (s == NULL)
return; /* illegal insertion of empty stuff */
int hv = hash (s->text);
hv = hash (s->text);
s->next = symbtab[hv];
symbtab[hv] = s;
}
@ -116,11 +118,14 @@ insert (Symbol s)
Symbol
lookup (char *s)
{
int hv;
Symbol t;
if (s == NULL)
return NULL;
int hv = hash (s);
Symbol t = symbtab[hv];
hv = hash (s);
t = symbtab[hv];
while (t != NULL)
{

4
src/termlists.c
View File

@ -220,12 +220,14 @@ termlistAppend (const Termlist tl, const Term term)
Termlist
termlistConcat (Termlist tl1, Termlist tl2)
{
Termlist scan;
if (tl1 == NULL)
return tl2;
if (tl2 == NULL)
return tl1;
Termlist scan = tl1;
scan = tl1;
while (scan->next != NULL)
scan = scan->next;
scan->next = tl2;

4
src/terms.c
View File

@ -90,7 +90,9 @@ makeTermTuple (Term t1, Term t2)
return NULL;
}
else
return t2;
{
return t2;
}
}
if (t2 == NULL)
{

4
src/tracebuf.c
View File

@ -104,13 +104,13 @@ tracebufInit (void)
void
tracebufDone (struct tracebuf *tb)
{
Roledef rd;
if (tb == NULL)
{
return;
}
Roledef rd;
varbufDone (tb->variables);
if (tb->length > 0)
{