From ca01a093778513f6a71e127e835bde7ce3319cc9 Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 26 May 2004 12:17:09 +0000 Subject: [PATCH] - Many ansi updates. --- src/knowledge.c | 8 +-- src/latex.c | 9 ++-- src/main.c | 22 +++++--- src/match_basic.c | 5 +- src/match_clp.c | 120 +++++++++++++++++++++++++------------------- src/output.c | 70 +++++++++++++------------- src/runs.c | 15 ++++-- src/substitutions.c | 4 +- src/symbols.c | 11 ++-- src/termlists.c | 4 +- src/terms.c | 4 +- src/tracebuf.c | 4 +- 12 files changed, 162 insertions(+), 114 deletions(-) diff --git a/src/knowledge.c b/src/knowledge.c index 765255a..d85f6cf 100644 --- a/src/knowledge.c +++ b/src/knowledge.c @@ -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; diff --git a/src/latex.c b/src/latex.c index 2b79959..74c63e5 100644 --- a/src/latex.c +++ b/src/latex.c @@ -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) diff --git a/src/main.c b/src/main.c index 122c58e..dfe3e8e 100644 --- a/src/main.c +++ b/src/main.c @@ -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); } + + diff --git a/src/match_basic.c b/src/match_basic.c index c55e2bd..bcb3c70 100644 --- a/src/match_basic.c +++ b/src/match_basic.c @@ -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)) { diff --git a/src/match_clp.c b/src/match_clp.c index 79a9c1f..1872a26 100644 --- a/src/match_clp.c +++ b/src/match_clp.c @@ -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; diff --git a/src/output.c b/src/output.c index 4c455ce..eae5b35 100644 --- a/src/output.c +++ b/src/output.c @@ -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++) diff --git a/src/runs.c b/src/runs.c index bf727c1..40a1c21 100644 --- a/src/runs.c +++ b/src/runs.c @@ -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); diff --git a/src/substitutions.c b/src/substitutions.c index 1c269db..3fd2abb 100644 --- a/src/substitutions.c +++ b/src/substitutions.c @@ -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)); diff --git a/src/symbols.c b/src/symbols.c index eacabc3..4470088 100644 --- a/src/symbols.c +++ b/src/symbols.c @@ -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) { diff --git a/src/termlists.c b/src/termlists.c index 12c76ac..df6bb39 100644 --- a/src/termlists.c +++ b/src/termlists.c @@ -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; diff --git a/src/terms.c b/src/terms.c index 7fca218..0fe6365 100644 --- a/src/terms.c +++ b/src/terms.c @@ -90,7 +90,9 @@ makeTermTuple (Term t1, Term t2) return NULL; } else - return t2; + { + return t2; + } } if (t2 == NULL) { diff --git a/src/tracebuf.c b/src/tracebuf.c index 484717f..9419753 100644 --- a/src/tracebuf.c +++ b/src/tracebuf.c @@ -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) {