diff --git a/src/arachne.c b/src/arachne.c index 918c61c..19e4222 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -110,17 +110,19 @@ arachneDone () #define isBound(rd) (rd->bind_run != INVALID) #define length step -#ifdef DEBUG //! Indent print void indentPrint () { +#ifdef DEBUG int i; for (i = 0; i < indentDepth; i++) eprintf ("| "); -} +#else + eprintf (">> "); #endif +} //! Iterate but discard the info of the termlist int @@ -384,15 +386,14 @@ bind_goal_regular (const Goal goal) } // Bind to all possible sends or intruder node; - return (iterate_role_sends (bind_this) && - add_intruder_goal_iterate (goal)); + return (iterate_role_sends (bind_this) && add_intruder_goal_iterate (goal)); } //! Bind an intruder goal to a regular run int bind_intruder_to_regular (const Goal goal) { - int bind_this (Protocol p, Role r, Roledef rd, int index) + int bind_this_f2 (Protocol p, Role r, Roledef rd, int index) { int element_f2 (Termlist substlist, Termlist keylist) { @@ -413,12 +414,12 @@ bind_intruder_to_regular (const Goal goal) * In any case, the list of keys is added as a new goal. */ int add_key_goal (Term t) - { - keygoals++; - create_intruder_goal (t); - //!@todo This needs a mapping Pi relation as well. - return 1; - } + { + keygoals++; + create_intruder_goal (t); + //!@todo This needs a mapping Pi relation as well. + return 1; + } keygoals = 0; termlist_iterate (keylist, add_key_goal); @@ -427,8 +428,13 @@ bind_intruder_to_regular (const Goal goal) * or from a new one. */ - flag = bind_existing_run (goal, p, r, index) && - bind_new_run (goal, p, r, index); + /** + * This code has a major bug (memory destruction) + * in both branches + *@todo FIX!! + */ + flag = bind_existing_run (goal, p, r, index) + && bind_new_run (goal, p, r, index); /** * deconstruct key list goals @@ -438,17 +444,18 @@ bind_intruder_to_regular (const Goal goal) roleInstanceDestroy (sys); keygoals--; } - + return flag; } } // Test for subterm unification - return termMguSubTerm (goal.rd->message, rd->message, element_f2, sys->traceKnow[0]->inverses, NULL); + return termMguSubTerm (goal.rd->message, rd->message, element_f2, + sys->traceKnow[0]->inverses, NULL); } // Bind to all possible sends? - return iterate_role_sends (bind_this); + return iterate_role_sends (bind_this_f2); } //! Bind an intruder goal by intruder construction diff --git a/src/mgu.c b/src/mgu.c index 6004c53..2f1cb98 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -198,7 +198,7 @@ termMguInTerm (Term t1, Term t2, int (*iterator) ()) */ int termMguSubTerm (Term t1, Term t2, int (*iterator) (), - const Termlist inverses, Termlist keylist) + Termlist inverses, Termlist keylist) { int flag; Termlist tl; @@ -230,8 +230,8 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (), // Recurse flag = - flag & termMguSubTerm (t1, t2->left.op, iterator, inverses, - keylist_new); + flag && termMguSubTerm (t1, t2->left.op, iterator, inverses, + keylist_new); termlistDelete (keylist_new); termDelete (newkey); @@ -242,7 +242,7 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (), if (tl != MGUFAIL) { // Iterate - flag = flag & iterator (tl, keylist); + flag = flag && iterator (tl, keylist); // Reset variables termlistSubstReset (tl); } diff --git a/src/mgu.h b/src/mgu.h index c9d03e5..f8f4bd0 100644 --- a/src/mgu.h +++ b/src/mgu.h @@ -17,7 +17,7 @@ Termlist termMguTerm (Term t1, Term t2); int termMguInTerm (Term t1, Term t2, int (*iterator) ()); int termMguSubTerm (Term t1, Term t2, int (*iterator) (), - const Termlist inverses, Termlist keylist); + Termlist inverses, Termlist keylist); void termlistSubstReset (Termlist tl); #endif