Removed unused functions.

src/arachne.c

@@ -1188,108 +1188,6 @@ bind_old_goal (const Binding b_new)
   return false;
 }
 
-//! Create a new intruder run to generate knowledge from m0
-int
-bind_goal_new_m0 (const Binding b)
-{
-  Termlist m0tl, tl;
-  int flag;
-  int found;
-
-
-  flag = 1;
-  found = 0;
-  m0tl = knowledgeSet (sys->know);
-  tl = m0tl;
-  while (flag && tl != NULL)
-    {
-      Term m0t;
-      Termlist subst;
-
-      m0t = tl->term;
-      subst = termMguTerm (b->term, m0t);	//! @todo This needs to be replace by the iterator one, but works for now
-      if (subst != MGUFAIL)
-	{
-	  int run;
-
-	  I_M->roledef->message = m0t;
-	  run = semiRunCreate (INTRUDER, I_M);
-	  proof_suppose_run (run, 0, 1);
-	  sys->runs[run].height = 1;
-	  {
-	    indentDepth++;
-	    if (goal_bind (b, run, 0))
-	      {
-		found++;
-		proof_suppose_binding (b);
-		if (switches.output == PROOF)
-		  {
-		    indentPrint ();
-		    eprintf ("* I.e. retrieving ");
-		    termPrint (b->term);
-		    eprintf (" from the initial knowledge.\n");
-		  }
-
-		{
-		  // Now we also want to add bindings to have this run before all other runs
-		  void wrapRunOrders (const int otherrun)
-		  {
-		    if (otherrun < 0)
-		      {
-			// No more runs to do
-			flag = flag && iterate ();
-		      }
-		    else
-		      {
-			if (otherrun != run)
-			  {
-			    if (dependPushEvent (run, 0, otherrun, 0))
-			      {
-				wrapRunOrders (otherrun - 1);
-				dependPopEvent ();
-			      }
-			  }
-			else
-			  {
-			    wrapRunOrders (otherrun - 1);
-			  }
-		      }
-		  }
-
-		  wrapRunOrders (sys->maxruns - 1);
-		}
-
-		goal_unbind (b);
-	      }
-	    else
-	      {
-		proof_cannot_bind (b, run, 0);
-	      }
-	    indentDepth--;
-	  }
-	  semiRunDestroy ();
-
-
-	  termlistSubstReset (subst);
-	  termlistDelete (subst);
-	}
-
-      tl = tl->next;
-    }
-
-  if (found == 0 && switches.output == PROOF)
-    {
-      indentPrint ();
-      eprintf ("Term ");
-      termPrint (b->term);
-      eprintf (" cannot be constructed from the initial knowledge.\n");
-    }
-  termlistDelete (m0tl);
-
-
-  return flag;
-}
-
 //! Bind an intruder goal by intruder composition construction
 /**
  * Handles the case where the intruder constructs a composed term himself.
@@ -1405,7 +1303,6 @@ bind_goal_new_intruder_run (const Binding b)
       eprintf (" from a new intruder run?\n");
     }
   indentDepth++;
-  //flag = bind_goal_new_m0 (b);
   //flag = flag && bind_goal_new_encrypt (b);
   flag = bind_goal_new_encrypt (b);
   indentDepth--;

src/binding.c

@@ -193,41 +193,6 @@ goal_unbind (const Binding b)
     }
 }
 
-//! Bind a goal as a dummy (block)
-/**
- * Especially made for tuple expansion
- *
- * @TODO Weird that this returns a value (always true, otherwise error)
- */
-int
-binding_block (Binding b)
-{
-  if (!b->blocked)
-    {
-      b->blocked = true;
-      return true;
-    }
-  error ("Trying to block a goal again.");
-  return false;
-}
-
-//! Unblock a binding
-/*
- * @TODO Weird that this returns a value (always true, otherwise error)
- */
-int
-binding_unblock (Binding b)
-{
-  if (b->blocked)
-    {
-      b->blocked = false;
-      return true;
-    }
-  error ("Trying to unblock a non-blocked goal.");
-  return false;
-}
-
-
 //! Add a goal
 /**
  * The int parameter 'level' is just to store additional info. Here, it stores priorities for a goal.

src/binding.h

@@ -27,6 +27,9 @@
 //! Binding structure
 /*
  * Idea is the ev_from *has to* precede the ev_to
+ *
+ * @TODO: blocked is no longer used. For evaluations, it may be considered
+ * false (no binding is ever blocked).
  */
 struct binding
 {

src/hidelevel.c

@@ -217,24 +217,6 @@ iterate_interesting (const System sys, const Term goalterm, int (*func) ())
   return true;
 }
 
-//! Determine whether a goal might be interesting from the viewpoint of hide levels (the highest minimum is best)
-int
-hidelevelInteresting (const System sys, const Term goalterm)
-{
-  int uninteresting (unsigned int l, unsigned int lmin, unsigned int lprot,
-		     unsigned int lknow)
-  {
-    if (lmin > 0)
-      {
-	// anything higher than usual is interesting :)
-	return false;
-      }
-    return true;
-  }
-
-  return !iterate_interesting (sys, goalterm, uninteresting);
-}
-
 //! Determine whether a goal is impossible to satisfy because of the hidelevel lemma.
 int
 hidelevelImpossible (const System sys, const Term goalterm)

src/hidelevel.h

@@ -39,7 +39,6 @@
  */
 
 void hidelevelCompute (const System sys);
-int hidelevelInteresting (const System sys, const Term goalterm);
 int hidelevelImpossible (const System sys, const Term goalterm);
 unsigned int hidelevelFlag (const System sys, const Term goalterm);
 

src/knowledge.c

@@ -316,26 +316,6 @@ inKnowledge (const Knowledge know, Term term)
   return 0;			/* unrecognized term type, weird */
 }
 
-//! Compare two knowledge sets.
-/**
- * This does not check currently for equivalence of inverse sets, which it should.
- *@return True iff both knowledge sets are equal.
- */
-int
-isKnowledgeEqual (Knowledge know1, Knowledge know2)
-{
-  if (know1 == NULL || know2 == NULL)
-    {
-      if (know1 == NULL && know2 == NULL)
-	return 1;
-      else
-	return 0;
-    }
-  if (!isTermlistEqual (know1->encrypt, know2->encrypt))
-    return 0;
-  return isTermlistEqual (know1->basic, know2->basic);
-}
-
 //! Print a knowledge set.
 void
 knowledgePrint (Knowledge know)
@@ -449,21 +429,6 @@ knowledgeGetInverses (const Knowledge know)
     return know->inverses;
 }
 
-//! Get all basic elements in the knowledge
-/**
- * This function is used by match_basic, to determine all basic elements in the knowledge set.
- * Most of the time this doesn't even change, so it might become a parameter of knowledge.
- * For now, this will have to do.
- *
- *@todo Investigate whether the basics in the knowledge set should be a parameter of knowledge, as it doesn't change very often.
- */
-__inline__ Termlist
-knowledgeGetBasics (const Knowledge know)
-{
-  return termlistAddBasics (termlistAddBasics (NULL, know->basic),
-			    know->encrypt);
-}
-
 //! check whether any substitutions where made in a knowledge set.
 /**
  * Typically, when a substitution is made, a knowledge set has to be reconstructed.
@@ -518,52 +483,3 @@ knowledgeSubstDo (const Knowledge know)
   /* otherwise a copy (for deletion) is returned. */
   return knowledgeReconstruction (know);
 }
-
-//! Undo substitutions that were not propagated yet.
-/**
- * Undo the substitutions just made. Note that this does not work anymore after knowledgeSubstDo()
- */
-void
-knowledgeSubstUndo (const Knowledge know)
-{
-  Termlist tl;
-
-  tl = know->vars;
-  while (tl != NULL)
-    {
-      tl->term->subst = NULL;
-      tl = tl->next;
-    }
-}
-
-//! Yield the minimal set of terms that are in some knowledge, but not in some other set.
-/**
- * Yield a termlist (or NULL) that represents the reduced items that are
- * in the new set, but not in the old one.
- *@param oldk The old knowledge.
- *@param newk The new knowledge, possibly with new terms.
- *@return A termlist of miminal terms in newk, but not in oldk.
- */
-
-Termlist
-knowledgeNew (const Knowledge oldk, const Knowledge newk)
-{
-  Termlist newtl;
-
-  void addNewStuff (Termlist tl)
-  {
-    while (tl != NULL)
-      {
-	if (!inKnowledge (oldk, tl->term))
-	  {
-	    newtl = termlistAdd (newtl, tl->term);
-	  }
-	tl = tl->next;
-      }
-  }
-
-  newtl = NULL;
-  addNewStuff (newk->basic);
-  addNewStuff (newk->encrypt);
-  return newtl;
-}

src/knowledge.h

@@ -63,14 +63,10 @@ int inKnowledge (const Knowledge know, Term term);
 void knowledgePrint (Knowledge know);
 void knowledgePrintShort (const Knowledge know);
 void knowledgeInversesPrint (Knowledge know);
-int isKnowledgeEqual (Knowledge know1, Knowledge know2);
 Termlist knowledgeSet (const Knowledge know);
 Termlist knowledgeGetInverses (const Knowledge know);
-Termlist knowledgeGetBasics (const Knowledge know);
 int knowledgeSubstNeeded (const Knowledge know);
 Knowledge knowledgeSubstDo (const Knowledge know);
-void knowledgeSubstUndo (const Knowledge know);
-Termlist knowledgeNew (const Knowledge oldk, const Knowledge newk);
 
 //! Harnass macro for recursive procedures.
 #define mindwipe(k,recurse) \

src/main.c

@@ -221,6 +221,7 @@ main (int argc, char **argv)
   knowledgeDestroy (sys->know);
   systemDone (sys);
   colorDone ();
+  switchesDone ();
   compilerDone ();
 
   /* done symbols */

src/mgu.h

@@ -32,7 +32,6 @@
  */
 #define MGUFAIL (Termlist) -1
 
-Termlist termMguTerm (Term t1, Term t2);
 void termlistSubstReset (Termlist tl);
 int checkRoletermMatch (const Term t1, const Term t2, const Termlist tl);
 

src/states.c

@@ -31,21 +31,6 @@ statesIncrease (const states_t states)
   return states + 1;
 }
 
-__inline__ double
-statesDouble (const states_t states)
-{
-  return (double) states;
-}
-
-__inline__ int
-statesSmallerThan (const states_t states, unsigned long int reflint)
-{
-  if (states < (states_t) reflint)
-    return 1;
-  else
-    return 0;
-}
-
 //! Sensible output for number of states/claims
 /**
  * Acts like a modified form of %g

src/states.h

@@ -32,9 +32,6 @@ typedef unsigned long int states_t;
 #define STATES0 0
 
 __inline__ states_t statesIncrease (const states_t states);
-__inline__ double statesDouble (const states_t states);
-__inline__ int statesSmallerThan (const states_t states,
-				  unsigned long int reflint);
 __inline__ void statesFormat (const states_t states);
 
 #endif

src/system.c

@@ -185,21 +185,6 @@ systemDone (const System sys)
   systemDestroy (sys);
 }
 
-//! Print a short version of the number of states.
-void
-statesPrintShort (const System sys)
-{
-  statesFormat (sys->states);
-}
-
-//! Print the number of states.
-void
-statesPrint (const System sys)
-{
-  statesFormat (sys->states);
-  eprintf (" states traversed.\n");
-}
-
 //! Destroy a system memory block and system::runs
 /**
  * Ignores any other substructes.
@@ -803,21 +788,6 @@ systemStart (const System sys)
     }
 }
 
-//! Activate indenting.
-void
-indentActivate ()
-{
-  indentState = 1;
-}
-
-//! Set indent depth.
-void
-indentSet (int i)
-{
-  if (indentState)
-    indentDepth = i;
-}
-
 //! Print the prefix of a line suitable for the current indent level.
 void
 indent ()
@@ -957,64 +927,6 @@ isRunTrusted (const System sys, const int run)
   return 1;
 }
 
-//! Yield the maximum length of a trace by analysing the runs in the system.
-int
-getMaxTraceLength (const System sys)
-{
-  Roledef rd;
-  int maxlen;
-  int run;
-
-  maxlen = 0;
-  for (run = 0; run < sys->maxruns; run++)
-    {
-      rd = runPointerGet (sys, run);
-      while (rd != NULL)
-	{
-	  rd = rd->next;
-	  maxlen++;
-	}
-    }
-  return maxlen;
-}
-
-//! Nicely format the role and agents we think we're talking to.
-void
-agentsOfRunPrint (const System sys, const int run)
-{
-  Term role = sys->runs[run].role->nameterm;
-  Termlist roles = sys->runs[run].protocol->rolenames;
-  int notfirst;
-
-  termPrint (role);
-  eprintf (":");
-  termPrint (agentOfRunRole (sys, run, role));
-  eprintf (" (");
-  notfirst = 0;
-  while (roles != NULL)
-    {
-      if (!isTermEqual (role, roles->term))
-	{
-	  if (notfirst)
-	    eprintf (", ");
-	  termPrint (roles->term);
-	  eprintf (":");
-	  termPrint (agentOfRunRole (sys, run, roles->term));
-	  notfirst = 1;
-	}
-      roles = roles->next;
-    }
-  eprintf (")");
-}
-
-//! Explain a violated claim at point i in the trace.
-
-void
-violatedClaimPrint (const System sys, const int i)
-{
-  eprintf ("Claim stuk");
-}
-
 void
 commandlinePrint (FILE * stream)
 {
@@ -1077,30 +989,6 @@ compute_roleeventmax (const System sys)
   return maxev;
 }
 
-//! Print the role, agents of a run
-void
-runInstancePrint (const System sys, const int run)
-{
-  termPrint (sys->runs[run].role->nameterm);
-  termlistPrint (sys->runs[run].rho);
-}
-
-//! Print an instantiated scenario (chooses and such)
-void
-scenarioPrint (const System sys)
-{
-  int run;
-
-  for (run = 0; run < sys->maxruns; run++)
-    {
-      runInstancePrint (sys, run);
-      if (run < sys->maxruns - 1)
-	{
-	  eprintf ("\t");
-	}
-    }
-}
-
 //! Determine whether we don't need any more attacks
 /**
  * Returns 1 (true) iff no more attacks are needed for this claim.

src/system.h

@@ -162,8 +162,6 @@ System systemInit ();
 void systemReset (const System sys);
 void systemRuns (const System sys);
 System systemDuplicate (const System fromsys);
-void statesPrint (const System sys);
-void statesPrintShort (const System sys);
 void systemDestroy (const System sys);
 void systemDone (const System sys);
 void ensureValidRun (const System sys, int run);
@@ -175,8 +173,6 @@ void roleInstance (const System sys, const Protocol protocol, const Role role,
 		   const Termlist paramlist, Termlist substlist);
 void roleInstanceDestroy (const System sys);
 void systemStart (const System sys);
-void indentActivate ();
-void indentSet (int i);
 void indent ();
 
 Protocol protocolCreate (Term nameterm);
@@ -184,15 +180,11 @@ void locVarPrint (Termlist tl);
 void protocolPrint (Protocol p);
 void protocolsPrint (Protocol p);
 int untrustedAgent (const System sys, Termlist agents);
-int getMaxTraceLength (const System sys);
-void agentsOfRunPrint (const System sys, const int run);
-void violatedClaimPrint (const System sys, int i);
 void commandlinePrint (FILE * stream);
 
 int compute_rolecount (const System sys);
 int compute_roleeventmax (const System sys);
 
-void scenarioPrint (const System sys);
 int isAgentTrusted (const System sys, Term agent);
 int isAgentlistTrusted (const System sys, Termlist agents);
 int isRunTrusted (const System sys, const int run);

src/tac.c

@@ -71,15 +71,6 @@ tacCreate (int op)
   return t;
 }
 
-Tac
-tacString (char *s)
-{
-  Tac t;
-  t = tacCreate (TAC_STRING);
-  t->t1.str = s;
-  return t;
-}
-
 Tac
 tacJoin (int op, Tac t1, Tac t2, Tac t3)
 {

src/termlist.c

@@ -762,40 +762,6 @@ termlistContained (const Termlist tlbig, Termlist tlsmall)
   return 1;
 }
 
-//! Check substitution validity
-/**
- * Determine whether a variable has been substituted with something with
- * the right type.
- *@param term The closed variable term.
- *@return True iff the substitution is valid in the current mode.
- *\sa system::match
- */
-
-int
-validSubst (const Term term)
-{
-  if (!realTermVariable (term) || term->subst == NULL)
-    return 1;
-  else
-    {
-      switch (switches.match)
-	{
-	case 0:		/* real type match */
-	  return realTermLeaf (term->subst)
-	    && termlistContained (term->stype, term->subst->stype);
-	case 1:		/* basic type match */
-	  /* subst must be a leaf */
-	  /* TODO: what about functions? */
-	  return realTermLeaf (term->subst);
-	case 2:		/* no type match */
-	  /* anything goes */
-	  return 1;
-	default:
-	  return 0;
-	}
-    }
-}
-
 //! Yield the result of f(x)
 /**
  * This function interpretes two termlists as the domain and range of a function,

src/type.c

@@ -148,41 +148,6 @@ checkTypeTerm (const Term tvar)
   return true;
 }
 
-//! Check types of a list
-/**
- * Empty list implies true.
- */
-int
-checkTypeTermlist (Termlist tl)
-{
-  while (tl != NULL)
-    {
-      if (!checkTypeTerm (tl->term))
-	return false;
-      tl = tl->next;
-    }
-  return true;
-}
-
-//! Check whether all local variables are instantiated correctly.
-int
-checkTypeLocals (const System sys)
-{
-  int run;
-
-  run = 0;
-  while (run < sys->maxruns)
-    {
-      if (sys->runs[run].protocol != INTRUDER)
-	{
-	  if (!checkTypeTermlist (sys->runs[run].locals))
-	    return false;
-	}
-      run++;
-    }
-  return true;
-}
-
 //! Check whether a typelist is a strict agent type list
 int
 isAgentType (Termlist typelist)

src/type.h

@@ -24,8 +24,6 @@
 #include "system.h"
 
 int checkTypeTerm (const Term t);
-int checkTypeTermlist (Termlist tl);
-int checkTypeLocals (const System sys);
 Termlist typelistConjunct (Termlist typelist1, Termlist Typelist2);
 int checkAllSubstitutions (const System sys);
 int isAgentType (Termlist typelist);

src/xmlout.c

@@ -915,12 +915,6 @@ xmlOutRuns (const System sys)
  * Publicly available functions
  */
 
-//! Output for a concrete trace (from modelchecker)
-void
-xmlOutTrace (const System sys)
-{
-}
-
 //! Output for a semitrace (from arachne method)
 /**
  * Note: Uses get_trace_length(), which is defined for the arachne method

src/xmlout.h

@@ -27,7 +27,6 @@ void xmlOutInit (void);
 void xmlOutDone (void);
 
 void xmlOutSemitrace (const System sys);
-void xmlOutTrace (const System sys);
 void xmlOutClaim (const System sys, Claimlist cl);
 
 #endif