diff --git a/src/arachne.c b/src/arachne.c index 3a7b663..b9c0d65 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -175,7 +175,7 @@ int isTermFunctionName (Term t) { t = deVar (t); - if (t != NULL && inTermlist (t->stype, TERM_Function)) + if (t != NULL && isTermLeaf(t) && inTermlist (t->stype, TERM_Function)) return 1; return 0; } @@ -1259,17 +1259,16 @@ bind_goal_regular_run (const Binding b) int flag; int found; + int test_sub_unification (Termlist substlist, Termlist keylist) + { + // A unification exists; return the signal + return 0; + } /* * This is a local function so we have access to goal */ int bind_this_role_send (Protocol p, Role r, Roledef rd, int index) { - int test_unification (Termlist substlist) - { - // A unification exists; return the signal - return 0; - } - if (p == INTRUDER) { // No intruder roles here @@ -1291,7 +1290,7 @@ bind_goal_regular_run (const Binding b) } #endif if (!termMguSubTerm - (b->term, rd->message, test_unification, sys->know->inverses, NULL)) + (b->term, rd->message, test_sub_unification, sys->know->inverses, NULL)) { int flag; diff --git a/src/mgu.c b/src/mgu.c index b6bfdd3..ba51db2 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -239,7 +239,7 @@ termMguTerm (Term t1, Term t2) *@returns Nothing. Iteration gets termlist of substitutions. */ int -termMguInTerm (Term t1, Term t2, int (*iterator) ()) +termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist)) { Termlist tl; int flag; @@ -282,16 +282,18 @@ termMguInTerm (Term t1, Term t2, int (*iterator) ()) *@returns Nothing. Iteration gets termlist of subst, and list of keys needed to decrypt. */ int -termMguSubTerm (Term t1, Term t2, int (*iterator) (), +termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist), Termlist inverses, Termlist keylist) { int flag; - Termlist tl; flag = 1; + t1 = deVar (t1); t2 = deVar (t2); if (t2 != NULL) { + Termlist tl; + if (!realTermLeaf (t2)) { if (realTermTuple (t2)) @@ -308,14 +310,14 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (), { // Must be encryption // So, we need the key, and try to get the rest - Termlist keylist_new; Term newkey; newkey = inverseKey (inverses, t2->right.key); - // We can never produce the TERM_Hidden key, thus, this is not a valid iteration. if (!isTermEqual (newkey, TERM_Hidden)) { + Termlist keylist_new; + keylist_new = termlistShallow (keylist); keylist_new = termlistAdd (keylist_new, newkey); @@ -343,7 +345,7 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (), } else { - if (deVar (t1) != NULL) + if (t1 != NULL) { flag = 0; } diff --git a/src/mgu.h b/src/mgu.h index f8f4bd0..3b2e04c 100644 --- a/src/mgu.h +++ b/src/mgu.h @@ -15,8 +15,8 @@ #define MGUFAIL (Termlist) -1 Termlist termMguTerm (Term t1, Term t2); -int termMguInTerm (Term t1, Term t2, int (*iterator) ()); -int termMguSubTerm (Term t1, Term t2, int (*iterator) (), +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);