- More cleanup and comments.

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;
-  Roledef rd = NULL;
   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;

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."); \
 				  }
 

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:
+      /* Now we add any role names to the agent list. Note that
-       * because if the variable is instantiated, the rolename will be as well, and thus they will
+       * instantiations do not matter: because if the variable is
-       * be equal anyway.
+       * 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);