From 3ca180d96836f04e80214cabfade9751a7d819b9 Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 8 Dec 2004 16:25:27 +0000 Subject: [PATCH] - Despite a full afternoon of debugging, semiRunCreate/Destroy still lose 8 blocks. I'm fairly confused. --- src/arachne.c | 160 ++++++++++++++------- src/binding.c | 378 ++++++++++++++++++++++++++++--------------------- src/memory.h | 16 +++ src/system.c | 55 +++++-- src/termlist.c | 15 +- src/termlist.h | 5 +- 6 files changed, 395 insertions(+), 234 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 20a52af..4740907 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -8,6 +8,10 @@ */ #include +#ifdef DEBUG +#include +#endif + #include "term.h" #include "termlist.h" #include "role.h" @@ -33,6 +37,7 @@ extern Term TERM_Function; extern int *graph; extern int nodes; +extern int graph_uordblks; static System sys; static Claimlist current_claim; @@ -113,9 +118,8 @@ arachneInit (const System mysys) */ INTRUDER = protocolCreate (makeGlobalConstant (" INTRUDER ")); - GVT = makeGlobalVariable ("GlobalVariable"); - add_event (SEND, GVT); + add_event (SEND, NULL); I_M = add_role ("I_M: Atomic message"); add_event (READ, NULL); @@ -667,14 +671,20 @@ bind_new_run (const Binding b, const Protocol p, const Role r, int flag; int newgoals; + findLoserBegin (graph_uordblks); run = semiRunCreate (p, r); proof_suppose_run (run, 0, index + 1); - newgoals = add_read_goals (run, 0, index + 1); - indentDepth++; - flag = bind_existing_to_goal (b, run, index); - indentDepth--; - goal_remove_last (newgoals); + { + findLoserBegin (graph_uordblks); + newgoals = add_read_goals (run, 0, index + 1); + indentDepth++; + flag = bind_existing_to_goal (b, run, index); + indentDepth--; + goal_remove_last (newgoals); + findLoserEnd (graph_uordblks, "bind_new_run: add read goals"); + } semiRunDestroy (); + findLoserEnd (graph_uordblks, "bind_new_run: inner"); return flag; } @@ -1280,55 +1290,67 @@ select_goal () int bind_goal_new_m0 (const Binding b) { - Termlist m0tl; + Termlist m0tl,tl; int flag; int found; + findLoserBegin(graph_uordblks); + flag = 1; found = 0; m0tl = knowledgeSet (sys->know); - while (flag && m0tl != NULL) + tl = m0tl; + while (flag && tl != NULL) { Term m0t; Termlist subst; + findLoserBegin (graph_uordblks); - m0t = m0tl->term; + m0t = tl->term; subst = termMguTerm (b->term, m0t); if (subst != MGUFAIL) { int run; + findLoserBegin (graph_uordblks); + I_M->roledef->message = b->term; run = semiRunCreate (INTRUDER, I_M); proof_suppose_run (run, 0, 1); - sys->runs[run].start->message = termDuplicate (b->term); sys->runs[run].length = 1; - indentDepth++; - if (goal_bind (b, run, 0)) { - found++; - proof_suppose_binding (b); - if (sys->output == PROOF) + findLoserBegin (graph_uordblks); + indentDepth++; + if (goal_bind (b, run, 0)) { - indentPrint (); - eprintf ("* I.e. retrieving "); - termPrint (b->term); - eprintf (" from the initial knowledge.\n"); + found++; + proof_suppose_binding (b); + if (sys->output == PROOF) + { + indentPrint (); + eprintf ("* I.e. retrieving "); + termPrint (b->term); + eprintf (" from the initial knowledge.\n"); + } + flag = flag && iterate (); } - flag = flag && iterate (); + else + { + proof_cannot_bind (b, run, 0); + } + goal_unbind (b); + indentDepth--; + findLoserEnd (graph_uordblks, "bind goal new m0 sugar core"); } - else - { - proof_cannot_bind (b, run, 0); - } - goal_unbind (b); - indentDepth--; semiRunDestroy (); + findLoserEnd (graph_uordblks, "bind goal new m0: inner loop 2"); + termlistSubstReset (subst); termlistDelete (subst); } - m0tl = m0tl->next; + tl = tl->next; + findLoserEnd(graph_uordblks, "bind goal new m0: inner loop"); } if (found == 0 && sys->output == PROOF) @@ -1339,6 +1361,9 @@ bind_goal_new_m0 (const Binding b) eprintf (" cannot be constructed from the initial knowledge.\n"); } termlistDelete (m0tl); + + findLoserEnd(graph_uordblks, "bind goal new m0"); + return flag; } @@ -1353,6 +1378,8 @@ bind_goal_new_encrypt (const Binding b) int flag; int can_be_encrypted; + findLoserBegin(graph_uordblks); + flag = 1; term = deVar (b->term); can_be_encrypted = 0; @@ -1396,21 +1423,25 @@ bind_goal_new_encrypt (const Binding b) termPrint (t2); eprintf ("\n"); } - newgoals = add_read_goals (run, 0, index + 1); + { // indenting purely added for findLoser + findLoserBegin(graph_uordblks); + newgoals = add_read_goals (run, 0, index + 1); - indentDepth++; - if (goal_bind (b, run, index)) - { - proof_suppose_binding (b); - flag = flag && iterate (); + indentDepth++; + if (goal_bind (b, run, index)) + { + proof_suppose_binding (b); + flag = flag && iterate (); + } + else + { + proof_cannot_bind (b, run, index); + } + goal_unbind (b); + indentDepth--; + goal_remove_last (newgoals); + findLoserEnd(graph_uordblks, "Goal bindings within m0 new"); } - else - { - proof_cannot_bind (b, run, index); - } - goal_unbind (b); - indentDepth--; - goal_remove_last (newgoals); semiRunDestroy (); } } @@ -1425,6 +1456,9 @@ bind_goal_new_encrypt (const Binding b) eprintf (" cannot be constructed by encryption.\n"); } } + + findLoserEnd(graph_uordblks, "bind goal new encrypt"); + return flag; } @@ -1496,6 +1530,7 @@ bind_goal_regular_run (const Binding b) NULL)) { int sflag; + findLoserBegin (graph_uordblks); // A good candidate found++; @@ -1522,8 +1557,13 @@ bind_goal_regular_run (const Binding b) // Bind to existing run sflag = bind_existing_run (b, p, r, index); // bind to new run - sflag = sflag && bind_new_run (b, p, r, index); + { + findLoserBegin (graph_uordblks); + sflag = sflag && bind_new_run (b, p, r, index); + findLoserEnd (graph_uordblks, "bind this role send; new run"); + } indentDepth--; + findLoserEnd (graph_uordblks, "bind this role send x"); return sflag; } else @@ -1604,6 +1644,7 @@ bind_goal (const Binding b) int know_only; Term function; + flag = 1; proof_select_goal (b); indentDepth++; @@ -1633,14 +1674,20 @@ bind_goal (const Binding b) proofDepth++; if (know_only) { + findLoserBegin (graph_uordblks); // Special case: only from intruder flag = flag && bind_goal_old_intruder_run (b); flag = flag && bind_goal_new_intruder_run (b); + findLoserEnd (graph_uordblks, "bind_goal intruder case"); } else { // Normal case - flag = bind_goal_regular_run (b); + { + findLoserBegin (graph_uordblks); + flag = bind_goal_regular_run (b); + findLoserEnd (graph_uordblks, "bind_goal case regular run"); + } flag = flag && bind_goal_old_intruder_run (b); flag = flag && bind_goal_new_intruder_run (b); } @@ -1773,14 +1820,19 @@ prune_theorems () } // Check for c-minimality - if (!bindings_c_minimal ()) { - if (sys->output == PROOF) + findLoserBegin(graph_uordblks); + if (!bindings_c_minimal ()) { - indentPrint (); - eprintf ("Pruned because this is not <=c-minimal.\n"); + if (sys->output == PROOF) + { + findLoserBegin(graph_uordblks); + indentPrint (); + eprintf ("Pruned because this is not <=c-minimal.\n"); + } + return 1; } - return 1; + findLoserEnd(graph_uordblks, "C-minimality test"); } /** @@ -2031,11 +2083,15 @@ iterate () { int flag; + findLoserBegin(graph_uordblks); + flag = 1; if (!prune_theorems ()) { + findLoserBegin(graph_uordblks); if (!prune_claim_specifics ()) { + findLoserBegin(graph_uordblks); if (!prune_bounds ()) { Binding b; @@ -2071,7 +2127,9 @@ iterate () /* * bind this goal in all possible ways and iterate */ + findLoserBegin (graph_uordblks); flag = bind_goal (b); + findLoserEnd (graph_uordblks, "bind_goal outer"); } } else @@ -2079,7 +2137,9 @@ iterate () // Pruned because of bound! current_claim->complete = 0; } + findLoserEnd(graph_uordblks, "just outside prune_bounds condition"); } + findLoserEnd(graph_uordblks, "just outside prune_claim_specifics condition"); } #ifdef DEBUG @@ -2088,6 +2148,10 @@ iterate () warning ("Flag has turned 0!"); } #endif + +#ifdef DEBUG + findLoserEnd (graph_uordblks, "iterate"); +#endif return flag; } diff --git a/src/binding.c b/src/binding.c index 047bb63..fa96069 100644 --- a/src/binding.c +++ b/src/binding.c @@ -12,10 +12,12 @@ #include "debug.h" #include "term.h" #include "termmap.h" +#include static System sys; -int *graph; -int nodes; +int *graph = NULL; +int nodes = 0; +int graph_uordblks = 0; extern Protocol INTRUDER; // The intruder protocol extern Role I_M; // special role; precedes all other events always @@ -38,8 +40,7 @@ binding_create (Term term, int run_to, int ev_to) b->ev_from = -1; b->run_to = run_to; b->ev_to = ev_to; - graph = NULL; - nodes = 0; + goal_graph_destroy(); b->term = term; b->level = 0; return b; @@ -68,6 +69,9 @@ bindingInit (const System mysys) { sys = mysys; sys->bindings = NULL; + graph = NULL; + nodes = 0; + graph_uordblks = 0; } //! Close up @@ -87,11 +91,27 @@ bindingDone () void goal_graph_destroy () { + findLoserBegin (graph_uordblks); if (graph != NULL) { +#ifdef DEBUG + struct mallinfo mi_free; + int mem_free; + + mi_free = mallinfo(); + mem_free = mi_free.uordblks; +#endif memFree (graph, (nodes * nodes) * sizeof (int)); graph = NULL; +#ifdef DEBUG + mi_free = mallinfo(); + if (mem_free - mi_free.uordblks != graph_uordblks) + error ("Freeing gave a weird result."); +#endif + graph_uordblks = 0; + nodes = 0; } + findLoserEnd (graph_uordblks, "goal_graph_destroy"); } //! Compute unclosed graph @@ -101,201 +121,229 @@ goal_graph_create () int run, ev; int last_m; List bl; + findLoserBegin (graph_uordblks); goal_graph_destroy (); // Setup graph nodes = node_count (); - graph = memAlloc ((nodes * nodes) * sizeof (int)); - graph_fill (graph, nodes, 0); - // Setup run order - run = 0; - last_m = -1; // last I_M run - while (run < sys->maxruns) { - ev = 1; - //!@todo This now reference to step, but we intend "length" as in Arachne. - while (ev < sys->runs[run].step) + struct mallinfo create_mi; + int create_mem_before; + + if (graph_uordblks != 0) + error ("Trying to create graph stuff without 0 uordblks for it first, but it is %i.", graph_uordblks); + findLoserBegin (graph_uordblks); + create_mi = mallinfo(); + create_mem_before = create_mi.uordblks; + graph = memAlloc ((nodes * nodes) * sizeof (int)); + create_mi = mallinfo(); + graph_uordblks = create_mi.uordblks - create_mem_before; + findLoserEnd (graph_uordblks, "core graph creation??"); + } + + { + findLoserBegin (graph_uordblks); + + graph_fill (graph, nodes, 0); + + // Setup run order + run = 0; + last_m = -1; // last I_M run + while (run < sys->maxruns) { - graph[graph_nodes (nodes, run, ev - 1, run, ev)] = 1; - ev++; - } - // Enforce I_M ordering - if (sys->runs[run].protocol == INTRUDER && sys->runs[run].role == I_M) - { - if (last_m != -1) + findLoserBegin (graph_uordblks); + ev = 1; + //!@todo This now reference to step, but we intend "length" as in Arachne. + while (ev < sys->runs[run].step) { - graph[graph_nodes (nodes, last_m, 0, run, 0)] = 1; + graph[graph_nodes (nodes, run, ev - 1, run, ev)] = 1; + ev++; } - last_m = run; - } - // Next - run++; - } - // Setup bindings order - bl = sys->bindings; - while (bl != NULL) - { - Binding b; - - b = (Binding) bl->data; - if (b->done) - { -#ifdef DEBUG - if (graph_nodes - (nodes, b->run_from, b->ev_from, b->run_to, - b->ev_to) >= (nodes * nodes)) - error ("Node out of scope for %i,%i -> %i,%i.\n", b->run_from, - b->ev_from, b->run_to, b->ev_to); -#endif - graph[graph_nodes - (nodes, b->run_from, b->ev_from, b->run_to, b->ev_to)] = 1; - } - bl = bl->next; - } - // Setup local constants order - run = 0; - while (run < sys->maxruns) - { - if (sys->runs[run].protocol != INTRUDER) - { - int run2; - - run2 = 0; - while (run2 < sys->maxruns) + // Enforce I_M ordering + if (sys->runs[run].protocol == INTRUDER && sys->runs[run].role == I_M) { - if (sys->runs[run].protocol != INTRUDER && run != run2) + if (last_m != -1) { - // For these two runs, we check whether run has any variables that are mapped - // to constants from run2 - Termlist tl; + graph[graph_nodes (nodes, last_m, 0, run, 0)] = 1; + } + last_m = run; + } + // Next + run++; + findLoserEnd (graph_uordblks, "goal_graph_create: runloop"); + } + // Setup bindings order + bl = sys->bindings; + while (bl != NULL) + { + findLoserBegin (graph_uordblks); + Binding b; - tl = sys->runs[run].locals; - while (tl != NULL) - { - Term t; - - t = tl->term; - if (t->type == VARIABLE && TermRunid (t) == run - && t->subst != NULL) - { - // t is a variable of run - Termlist tl2; - - tl2 = sys->runs[run2].locals; - while (tl2 != NULL) - { - Term t2; - - t2 = tl2->term; - if (realTermLeaf (t2) && t2->type != VARIABLE - && TermRunid (t2) == run2) - { - // t2 is a constant of run2 - if (isTermEqual (t, t2)) - { - // Indeed, run depends on the run2 constant t2. Thus we must store this order. - // The first send of t2 in run2 must be before the first (read) event in run with t2. - int ev2; - int done; - Roledef rd2; - - done = 0; - ev2 = 0; - rd2 = sys->runs[run2].start; - while (!done - && ev2 < sys->runs[run2].step) - { - if (rd2->type == SEND - && termSubTerm (rd2->message, - t2)) - { - // Allright, we send it here at ev2 first - int ev; - Roledef rd; - - ev = 0; - rd = sys->runs[run].start; - while (!done - && ev < - sys->runs[run].step) - { - if (termSubTerm - (rd->message, t2)) - { - // Term occurs here in run - if (rd->type == READ) - { - // It's read here first. - // Order and be done with it. - graph[graph_nodes - (nodes, run2, - ev2, run, - ev)] = 1; + b = (Binding) bl->data; + if (b->done) + { #ifdef DEBUG - if (DEBUGL (5)) - { - eprintf - ("* [local originator] term "); - termPrint (t2); - eprintf - (" is bound using %i, %i before %i,%i\n", - run2, ev2, - run, ev); - } + if (graph_nodes + (nodes, b->run_from, b->ev_from, b->run_to, + b->ev_to) >= (nodes * nodes)) + error ("Node out of scope for %i,%i -> %i,%i.\n", b->run_from, + b->ev_from, b->run_to, b->ev_to); #endif - done = 1; - } - else + graph[graph_nodes + (nodes, b->run_from, b->ev_from, b->run_to, b->ev_to)] = 1; + } + bl = bl->next; + findLoserEnd (graph_uordblks, "goal_graph_create: bindings loop"); + } + // Setup local constants order + run = 0; + while (run < sys->maxruns) + { + findLoserBegin (graph_uordblks); + if (sys->runs[run].protocol != INTRUDER) + { + int run2; + + run2 = 0; + while (run2 < sys->maxruns) + { + if (sys->runs[run].protocol != INTRUDER && run != run2) + { + // For these two runs, we check whether run has any variables that are mapped + // to constants from run2 + Termlist tl; + + tl = sys->runs[run].locals; + while (tl != NULL) + { + Term t; + + t = tl->term; + if (t->type == VARIABLE && TermRunid (t) == run + && t->subst != NULL) + { + // t is a variable of run + Termlist tl2; + + tl2 = sys->runs[run2].locals; + while (tl2 != NULL) + { + Term t2; + + t2 = tl2->term; + if (realTermLeaf (t2) && t2->type != VARIABLE + && TermRunid (t2) == run2) + { + // t2 is a constant of run2 + if (isTermEqual (t, t2)) + { + // Indeed, run depends on the run2 constant t2. Thus we must store this order. + // The first send of t2 in run2 must be before the first (read) event in run with t2. + int ev2; + int done; + Roledef rd2; + + done = 0; + ev2 = 0; + rd2 = sys->runs[run2].start; + while (!done + && ev2 < sys->runs[run2].step) + { + if (rd2->type == SEND + && termSubTerm (rd2->message, + t2)) + { + // Allright, we send it here at ev2 first + int ev; + Roledef rd; + + ev = 0; + rd = sys->runs[run].start; + while (!done + && ev < + sys->runs[run].step) + { + if (termSubTerm + (rd->message, t2)) { - // It doesn't occur first in a READ, which shouldn't be happening - if (sys->output == - PROOF) + // Term occurs here in run + if (rd->type == READ) { - eprintf - ("Term "); - termPrint (t2); - eprintf - (" from run %i occurs in run %i, term ", - run2, run); - termPrint (t); - eprintf - (" before it is read?\n"); + // It's read here first. + // Order and be done with it. + graph[graph_nodes + (nodes, run2, + ev2, run, + ev)] = 1; +#ifdef DEBUG + if (DEBUGL (5)) + { + eprintf + ("* [local originator] term "); + termPrint (t2); + eprintf + (" is bound using %i, %i before %i,%i\n", + run2, ev2, + run, ev); + } +#endif + done = 1; } - // Thus, we create an artificial loop - if (sys->runs[0]. - step > 1) + else { - // This forces a loop, and thus prunes - graph - [graph_nodes - (nodes, 0, 1, - 0, 0)] = 1; + // It doesn't occur first in a READ, which shouldn't be happening + if (sys->output == + PROOF) + { + eprintf + ("Term "); + termPrint (t2); + eprintf + (" from run %i occurs in run %i, term ", + run2, run); + termPrint (t); + eprintf + (" before it is read?\n"); + } + // Thus, we create an artificial loop + if (sys->runs[0]. + step > 1) + { + // This forces a loop, and thus prunes + graph + [graph_nodes + (nodes, 0, 1, + 0, 0)] = 1; + } } } + rd = rd->next; + ev++; } - rd = rd->next; - ev++; + done = 1; } - done = 1; + rd2 = rd2->next; + ev2++; } - rd2 = rd2->next; - ev2++; } } + tl2 = tl2->next; } - tl2 = tl2->next; } + tl = tl->next; } - tl = tl->next; } + run2++; } - run2++; } + run++; + findLoserEnd (graph_uordblks, "goal_graph_create local constants loop"); } - run++; + findLoserEnd (graph_uordblks, "goal_graph_create: constructing graph innards"); } + findLoserEnd (graph_uordblks, "goal_graph_create"); } diff --git a/src/memory.h b/src/memory.h index e8aa199..4e80487 100644 --- a/src/memory.h +++ b/src/memory.h @@ -11,4 +11,20 @@ void memDone (); #define memFree(p,t) free(p) #define memRealloc(p,t) realloc(p,t); +#define findLoserBegin(ign) int mem_before; \ + int mem_diff; \ + static int mem_errorcount = 0; \ + struct mallinfo mi; \ + mi = mallinfo(); \ + mem_before = mi.uordblks - ign; +#define findLoserEnd(ign,t) mi = mallinfo(); \ + mem_diff = mi.uordblks - ign - mem_before; \ + if (mem_diff != 0) \ + { \ + warning ("Memory leak in [%s] of %i", t, mem_diff); \ + mem_errorcount++; \ + if (mem_errorcount >= 10) \ + error ("More than enough leaks."); \ + } + #endif diff --git a/src/system.c b/src/system.c index 2cc2524..9b13eb9 100644 --- a/src/system.c +++ b/src/system.c @@ -589,12 +589,18 @@ run_localize (const System sys, const int rid, Termlist fromlist, rd = sys->runs[rid].start; while (rd != NULL) { - rd->from = termLocal (rd->from, fromlist, tolist, rid); - rd->to = termLocal (rd->to, fromlist, tolist, rid); - rd->message = termLocal (rd->message, fromlist, tolist, rid); + rd->from = termLocal (rd->from, fromlist, tolist); + rd->to = termLocal (rd->to, fromlist, tolist); + rd->message = termLocal (rd->message, fromlist, tolist); rd = rd->next; } + // Substlist is NULL currently? No usage of this last stuff now + // TODO + if (substlist != NULL) + { + error ("Substlist should be NULL in run_localize"); + } sys->runs[rid].substitutions = NULL; while (substlist != NULL) { @@ -603,7 +609,7 @@ run_localize (const System sys, const int rid, Termlist fromlist, t = substlist->term; if (t->subst != NULL) { - t->subst = termLocal (t->subst, fromlist, tolist, rid); + t->subst = termLocal (t->subst, fromlist, tolist); sys->runs[rid].substitutions = termlistAdd (sys->runs[rid].substitutions, t); } @@ -668,7 +674,7 @@ roleInstanceArachne (const System sys, const Protocol protocol, { // Make new var for this run newt = makeTermType (VARIABLE, TermSymb (newt), rid); - artefacts = termlistAdd (artefacts, newt); + artefacts = termlistAddNew (artefacts, newt); newt->stype = oldt->stype; // Copy substitution newt->subst = oldt->subst; @@ -695,7 +701,8 @@ roleInstanceArachne (const System sys, const Protocol protocol, else { extterm = makeTermTuple (newt, extterm); - artefacts = termlistAdd (artefacts, extterm); + // NOTE: don't these get double deleted? By roledefdestroy? + artefacts = termlistAddNew (artefacts, extterm); } } } @@ -728,10 +735,10 @@ roleInstanceArachne (const System sys, const Protocol protocol, newt = create_new_local (t, rid); if (newt != NULL) { - artefacts = termlistAdd (artefacts, newt); + artefacts = termlistAddNew (artefacts, newt); if (realTermVariable (newt)) { - sys->variables = termlistAdd (sys->variables, newt); + sys->variables = termlistAddNew (sys->variables, newt); } fromlist = termlistAdd (fromlist, t); tolist = termlistAdd (tolist, newt); @@ -967,13 +974,41 @@ roleInstanceDestroy (const System sys) } substlist = substlist->next; } + termlistDelete(myrun.substitutions); + + // sys->variables might contain locals from the run: remove them + { + Termlist tl; + + tl = sys->variables; + while (tl != NULL) + { + Term t; + + t = tl->term; + if (TermRunid(t) == runid) + { + // remove from list; return pointer to head + sys->variables = termlistDelTerm (tl); + tl = sys->variables; + } + else + { + // proceed + tl = tl->next; + } + } + } + + // remove lists termlistDelete (myrun.artefacts); termlistDelete (myrun.locals); termlistDelete (myrun.agents); + // Destroy run struct allocation in array using realloc - sys->runs = (Run) memRealloc (sys->runs, sizeof (struct run) * (runid)); // Reduce run count - sys->maxruns = runid; + sys->maxruns = sys->maxruns - 1; + sys->runs = (Run) memRealloc (sys->runs, sizeof (struct run) * (sys->maxruns)); } } diff --git a/src/termlist.c b/src/termlist.c index 8d5fe42..30a7b11 100644 --- a/src/termlist.c +++ b/src/termlist.c @@ -621,7 +621,7 @@ inverseKey (Termlist inverses, Term key) *\sa termlistLocal() */ Term -termLocal (Term t, Termlist fromlist, Termlist tolist, const int runid) +termLocal (Term t, Termlist fromlist, Termlist tolist) { if (t == NULL) return NULL; @@ -645,13 +645,13 @@ termLocal (Term t, Termlist fromlist, Termlist tolist, const int runid) Term newt = termNodeDuplicate (t); if (realTermTuple (t)) { - TermOp1 (newt) = termLocal (TermOp1 (t), fromlist, tolist, runid); - TermOp2 (newt) = termLocal (TermOp2 (t), fromlist, tolist, runid); + TermOp1 (newt) = termLocal (TermOp1 (t), fromlist, tolist); + TermOp2 (newt) = termLocal (TermOp2 (t), fromlist, tolist); } else { - TermOp (newt) = termLocal (TermOp (t), fromlist, tolist, runid); - TermKey (newt) = termLocal (TermKey (t), fromlist, tolist, runid); + TermOp (newt) = termLocal (TermOp (t), fromlist, tolist); + TermKey (newt) = termLocal (TermKey (t), fromlist, tolist); } return newt; } @@ -663,15 +663,14 @@ termLocal (Term t, Termlist fromlist, Termlist tolist, const int runid) *\sa termLocal() */ Termlist -termlistLocal (Termlist tl, const Termlist fromlist, const Termlist tolist, - int runid) +termlistLocal (Termlist tl, const Termlist fromlist, const Termlist tolist) { Termlist newtl = NULL; while (tl != NULL) { newtl = - termlistAdd (newtl, termLocal (tl->term, fromlist, tolist, runid)); + termlistAdd (newtl, termLocal (tl->term, fromlist, tolist)); tl = tl->next; } return newtl; diff --git a/src/termlist.h b/src/termlist.h index 748ad0a..254c809 100644 --- a/src/termlist.h +++ b/src/termlist.h @@ -46,10 +46,9 @@ Termlist termlistAddBasics (Termlist tl, Termlist scan); Termlist termlistMinusTerm (Termlist tl, Term t); int termlistLength (Termlist tl); Term inverseKey (Termlist inverses, Term key); -Term termLocal (const Term t, Termlist fromlist, Termlist tolist, - const int runid); +Term termLocal (const Term t, Termlist fromlist, Termlist tolist); Termlist termlistLocal (Termlist tl, const Termlist fromlist, - const Termlist tolist, const int runid); + const Termlist tolist); int termlistContained (const Termlist tlbig, Termlist tlsmall); int validSubst (const int matchmode, const Term term); Term termFunction (Termlist fromlist, Termlist tolist, Term tx);