diff --git a/gui/Scyther/Bin/scyther-linux b/gui/Scyther/Bin/scyther-linux index 3a74461..75e0db7 100755 Binary files a/gui/Scyther/Bin/scyther-linux and b/gui/Scyther/Bin/scyther-linux differ diff --git a/src/compiler.c b/src/compiler.c index 0a4768a..8cdfe2c 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -1950,7 +1950,8 @@ checkWellFormed (const System sys) //! Check matching role defs int -checkEventMatch (const Roledef rd1, const Roledef rd2) +checkEventMatch (const Roledef rd1, const Roledef rd2, + const Termlist rolenames) { if (!isTermEqual (rd1->from, rd2->from)) { @@ -1960,7 +1961,7 @@ checkEventMatch (const Roledef rd1, const Roledef rd2) { return false; } - if (!checkRoletermMatch (rd1->message, rd2->message)) + if (!checkRoletermMatch (rd1->message, rd2->message, rolenames)) { return false; } @@ -1992,7 +1993,7 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole, if (isTermEqual (event->label, readevent->label)) { // Same labels, so they should match up! - if (!checkEventMatch (event, readevent)) + if (!checkEventMatch (event, readevent, p->rolenames)) { globalError++; eprintf ("error: [%i]", readevent->lineno); diff --git a/src/mgu.c b/src/mgu.c index 0014de2..679db67 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -581,9 +581,12 @@ termMguSubTerm (Term smallterm, Term bigterm, return flag; } -//! Check if terms might match in some way +//! Check if role terms might match in some way +/** + * Interesting case: role names are variables here, so they always match. We catch that case by inspecting the variable list. + */ int -checkRoletermMatch (const Term t1, const Term t2) +checkRoletermMatch (const Term t1, const Term t2, const Termlist notmapped) { Termlist tl; @@ -595,10 +598,27 @@ checkRoletermMatch (const Term t1, const Term t2) } else { + int result; + Termlist vl; + + result = true; // Reset variables termlistSubstReset (tl); + // Check variable list etc: should not contain mapped role names + vl = tl; + while (vl != NULL) + { + // This term should not be in the notmapped list + if (inTermlist (notmapped, vl->term)) + { + result = false; + break; + } + vl = vl->next; + + } // Remove list termlistDelete (tl); - return true; + return result; } } diff --git a/src/mgu.h b/src/mgu.h index 01eb7a9..42ac00e 100644 --- a/src/mgu.h +++ b/src/mgu.h @@ -19,7 +19,7 @@ int termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist)); int termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist), Termlist inverses, Termlist keylist); void termlistSubstReset (Termlist tl); -int checkRoletermMatch (Term t1, Term t2); +int checkRoletermMatch (const Term t1, const Term t2, const Termlist tl); // The new iteration methods int unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist)); diff --git a/src/parser.y b/src/parser.y index c0027ae..6992928 100644 --- a/src/parser.y +++ b/src/parser.y @@ -318,7 +318,7 @@ int yyerror(char *s) extern int yylineno; //!< defined and maintained in lex.c extern char *yytext; //!< defined and maintained in lex.c - error ("%s at symbol '%s' on line %i.\n", s, yytext, yylineno); + error ("[%i] %s at symbol '%s'.\n", yylineno, s, yytext); return 0; }