diff --git a/src/arachne.c b/src/arachne.c index 4740907..7cbf891 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -45,12 +45,6 @@ static int attack_length; Protocol INTRUDER; // Pointers, to be set by the Init Role I_M; // Same here. -Role I_F; -Role I_T; -Role I_V; -Role I_R; -Role I_E; -Role I_D; Role I_RRS; static int indentDepth; @@ -83,8 +77,7 @@ void printSemiState (); void arachneInit (const System mysys) { - Term GVT; - Roledef rd = NULL; + Roledef rd; Termlist tl, know0; void add_event (int event, Term message) @@ -119,6 +112,9 @@ arachneInit (const System mysys) INTRUDER = protocolCreate (makeGlobalConstant (" INTRUDER ")); + // Initially empty roledef + rd = NULL; + add_event (SEND, NULL); I_M = add_role ("I_M: Atomic message"); @@ -1313,7 +1309,7 @@ bind_goal_new_m0 (const Binding b) int run; findLoserBegin (graph_uordblks); - I_M->roledef->message = b->term; + I_M->roledef->message = m0t; run = semiRunCreate (INTRUDER, I_M); proof_suppose_run (run, 0, 1); sys->runs[run].length = 1; diff --git a/src/memory.h b/src/memory.h index 4e80487..a7a3039 100644 --- a/src/memory.h +++ b/src/memory.h @@ -23,7 +23,7 @@ void memDone (); { \ warning ("Memory leak in [%s] of %i", t, mem_diff); \ mem_errorcount++; \ - if (mem_errorcount >= 10) \ + if (mem_errorcount >= 1) \ error ("More than enough leaks."); \ } diff --git a/src/system.c b/src/system.c index c488de9..1c41abe 100644 --- a/src/system.c +++ b/src/system.c @@ -258,36 +258,40 @@ ensureValidRun (const System sys, int run) /* (re)allocate space */ /* Note, this is never explicitly freed, because it is never copied */ - - sys->runs = (Run) memRealloc (sys->runs, sizeof (struct run) * (run + 1)); - /* update size parameter */ oldsize = sys->maxruns; sys->maxruns = run + 1; + sys->runs = (Run) memRealloc (sys->runs, sizeof (struct run) * (sys->maxruns)); /* create runs, set the new pointer(s) to NULL */ for (i = oldsize; i < sys->maxruns; i++) { /* init run */ struct run myrun = sys->runs[i]; + myrun.protocol = NULL; myrun.role = NULL; myrun.agents = NULL; myrun.step = 0; myrun.index = NULL; myrun.start = NULL; + + myrun.locals = NULL; + myrun.artefacts = NULL; + myrun.substitutions = NULL; + if (sys->engine == POR_ENGINE) { myrun.know = knowledgeDuplicate (sys->know); - myrun.prevSymmRun = -1; - myrun.firstNonAgentRead = -1; } else { // Arachne etc. myrun.know = NULL; - myrun.prevSymmRun = -1; - myrun.firstNonAgentRead = -1; } + + myrun.prevSymmRun = -1; + myrun.firstNonAgentRead = -1; + myrun.firstReal = 0; } } @@ -686,9 +690,10 @@ roleInstanceArachne (const System sys, const Protocol protocol, artefacts = termlistAddNew (artefacts, newt); newt->stype = oldt->stype; } - /* Now we add any role names to the agent list. Note that instantiations do not matter: - * because if the variable is instantiated, the rolename will be as well, and thus they will - * be equal anyway. + /* Now we add any role names to the agent list. Note that + * instantiations do not matter: because if the variable is + * instantiated, the rolename will be as well, and thus they will be + * equal anyway. */ if (inTermlist (protocol->rolenames, oldt)) { @@ -730,6 +735,10 @@ roleInstanceArachne (const System sys, const Protocol protocol, scanfrom = scanfrom->next; } + /* Now we prefix the read before rd, if extterm is not NULL. Even if + * extterm is NULL, rd is still set as the start and the index pointer of + * the run. + */ run_prefix_read (sys, rid, rd, extterm); /* duplicate all locals form this run */ @@ -995,7 +1004,7 @@ roleInstanceDestroy (const System sys) Term t; t = tl->term; - if (TermRunid(t) == runid) + if (realTermLeaf(t) && TermRunid(t) == runid) { // remove from list; return pointer to head sys->variables = termlistDelTerm (tl);