- Fixed intruder generated value displays.

src/arachne.c

@@ -1740,6 +1740,9 @@ createNewTermGeneric (Termlist tl, Term t)
   memcpy (newterm, t, sizeof (struct term));
   TermRunid (newterm) = freenumber;
 
+  /* The type of the new term should be that of the parent! */
+  newterm->stype = termlistAppend (NULL, t);
+
   /* return */
   return termlistPrepend (tl, newterm);
 }

src/dotout.c

@@ -5,6 +5,7 @@
 #include "arachne.h"
 #include "binding.h"
 #include "depend.h"
+#include "type.h"
 #include "debug.h"
 
 extern Protocol INTRUDER;	// Pointers, to be set by the Init of arachne.c
@@ -63,8 +64,29 @@ static System sys = NULL;
  * code
  */
 
+//! Is this term chosen by the intruder?
+int
+isIntruderChoice (const Term t)
+{
+  if (realTermLeaf (t))
+    {
+      if (TermRunid (t) >= sys->maxruns)
+	{
+	  // Chosen by intruder
+	  // However, if it is a rolename, this is not really what we mean
+	  if (!(t->roleVar || isAgentType (t->stype)))
+	    {
+	      // Not a role variable, and chosen by the intruder: that's it
+	      return true;
+	    }
+	}
+    }
+  return false;
+}
+
+//! Print the run identifier in some meaningful way
 void
-printVisualRun (int rid)
+printVisualRunID (int rid)
 {
   int run;
   int displayi;
@@ -99,11 +121,20 @@ printVisualRun (int rid)
     }
   else
     {
-      // >= sys->maxruns means intruder choice
+      eprintf ("%i", (rid - sys->maxruns + 1));
-      eprintf ("Intruder%i", (rid - sys->maxruns + 1));
     }
 }
 
+void
+printVisualRun (const Term t)
+{
+  if (isIntruderChoice (t))
+    {
+      eprintf ("Intruder");
+    }
+  printVisualRunID (TermRunid (t));
+}
+
 //! Remap term stuff
 void
 termPrintRemap (const Term t)
@@ -113,12 +144,16 @@ termPrintRemap (const Term t)
 
 //! Remap term list
 void
-termlistPrintRemap (Termlist tl)
+termlistPrintRemap (Termlist tl, char *sep)
 {
   while (tl != NULL)
     {
-      termPrintRemap(tl->term);
+      termPrintRemap (tl->term);
       tl = tl->next;
+      if (tl != NULL)
+	{
+	  eprintf ("%s", sep);
+	}
     }
 }
 
@@ -1263,7 +1298,7 @@ printRunExplanation (const System sys, const int run,
   int hadcontent;
 
   eprintf ("Run ");
-  printVisualRun (run);
+  printVisualRunID (run);
 
   eprintf (runrolesep);
   // Print first line
@@ -1700,57 +1735,55 @@ dotSemiState (const System mysys)
   from_intruder_count = drawAllBindings (sys);
 
   // Third, the intruder node (if needed)
-    {
+  {
-  /*
+    /*
-   * Stupid brute analysis, can probably be done much more efficient, but
+     * Stupid brute analysis, can probably be done much more efficient, but
-   * this is not a timing critical bit, so we just do it like this.
+     * this is not a timing critical bit, so we just do it like this.
-   */
+     */
-  Termlist found;
+    Termlist found;
-  List bl;
+    List bl;
 
-  // collect the intruder-generated constants
+    // collect the intruder-generated constants
-  found = NULL;
+    found = NULL;
-  for (bl = sys->bindings; bl != NULL; bl = bl->next)
+    for (bl = sys->bindings; bl != NULL; bl = bl->next)
-    {
+      {
-      Binding b;
+	Binding b;
 
-      b = (Binding) bl->data;
+	b = (Binding) bl->data;
-      if (!b->blocked)
+	if (!b->blocked)
-	{
+	  {
-	  int addsubterms(Term t)
+	    int addsubterms (Term t)
 	    {
-	      if (TermRunid(t) >= sys->maxruns)
+	      if (isIntruderChoice (t))
 		{
-                  // >= sys->maxruns means intruder choice
+		  found = termlistAddNew (found, t);
-	          found = termlistAddNew(found, t);
 		}
 	      return true;
 	    }
 
-	  term_iterate_open_leaves(b->term, addsubterms);
+	    term_iterate_open_leaves (b->term, addsubterms);
-	}
+	  }
-    }
+      }
 
-  // now maybe we draw the node
+    // now maybe we draw the node
-  if ((from_intruder_count > 0) || (found != NULL))
+    if ((from_intruder_count > 0) || (found != NULL))
-    {
+      {
-      eprintf
+	eprintf ("\tintruder [\n");
-	("\tintruder [\n");
+	eprintf ("\t\tlabel=\"");
-      eprintf ("\t\tlabel=\"");
+	eprintf ("Initial intruder knowledge");
-      eprintf ("Initial intruder knowledge");
+	if (found != NULL)
-      if (found != NULL)
+	  {
-	{
+	    eprintf ("\\n");
-	  eprintf ("\\n");
+	    eprintf ("The intruder generates: ");
-	  eprintf ("The intruder generates: ");
+	    termlistPrintRemap (found, ", ");
-	  termlistPrintRemap (found);
+	  }
-	}
+	eprintf ("\",\n");
-      eprintf ("\",\n");
+	eprintf ("\t\tstyle=filled,fillcolor=\"");
-      eprintf ("\t\tstyle=filled,fillcolor=\"");
+	printColor (INTRUDERCOLORH, INTRUDERCOLORL, INTRUDERCOLORS);
-      printColor (INTRUDERCOLORH, INTRUDERCOLORL, INTRUDERCOLORS);
+	eprintf ("\"\n\t];\n");
-      eprintf ("\"\n\t];\n");
+      }
-    }
+    termlistDelete (found);
-  termlistDelete(found);
+  }
-    }
 
   // eprintf ("\t};\n");
 

src/parser.h

@@ -1,7 +1,9 @@
-/* A Bison parser, made by GNU Bison 2.1.  */
+/* A Bison parser, made by GNU Bison 2.3.  */
 
-/* Skeleton parser for Yacc-like parsing with Bison,
+/* Skeleton interface for Bison's Yacc-like parsers in C
-   Copyright (C) 1984, 1989, 1990, 2000, 2001, 2002, 2003, 2004, 2005 Free Software Foundation, Inc.
+
+   Copyright (C) 1984, 1989, 1990, 2000, 2001, 2002, 2003, 2004, 2005, 2006
+   Free Software Foundation, Inc.
 
    This program is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
@@ -18,37 +20,46 @@
    Foundation, Inc., 51 Franklin Street, Fifth Floor,
    Boston, MA 02110-1301, USA.  */
 
-/* As a special exception, when this file is copied by Bison into a
+/* As a special exception, you may create a larger work that contains
-   Bison output file, you may use that output file without restriction.
+   part or all of the Bison parser skeleton and distribute that work
-   This special exception was added by the Free Software Foundation
+   under terms of your choice, so long as that work isn't itself a
-   in version 1.24 of Bison.  */
+   parser generator using the skeleton or a modified version thereof
+   as a parser skeleton.  Alternatively, if you modify or redistribute
+   the parser skeleton itself, you may (at your option) remove this
+   special exception, which will cause the skeleton and the resulting
+   Bison output files to be licensed under the GNU General Public
+   License without this special exception.
+
+   This special exception was added by the Free Software Foundation in
+   version 2.2 of Bison.  */
 
 /* Tokens.  */
 #ifndef YYTOKENTYPE
 # define YYTOKENTYPE
    /* Put the tokens into the symbol table, so that GDB and other debuggers
       know about them.  */
-   enum yytokentype {
+enum yytokentype
-     ID = 258,
+{
-     PROTOCOL = 259,
+  ID = 258,
-     ROLE = 260,
+  PROTOCOL = 259,
-     READT = 261,
+  ROLE = 260,
-     SENDT = 262,
+  READT = 261,
-     CLAIMT = 263,
+  SENDT = 262,
-     VAR = 264,
+  CLAIMT = 263,
-     CONST = 265,
+  VAR = 264,
-     RUN = 266,
+  CONST = 265,
-     SECRET = 267,
+  RUN = 266,
-     COMPROMISED = 268,
+  SECRET = 267,
-     INVERSEKEYS = 269,
+  COMPROMISED = 268,
-     UNTRUSTED = 270,
+  INVERSEKEYS = 269,
-     USERTYPE = 271,
+  UNTRUSTED = 270,
-     SINGULAR = 272,
+  USERTYPE = 271,
-     FUNCTION = 273,
+  SINGULAR = 272,
-     HASHFUNCTION = 274,
+  FUNCTION = 273,
-     KNOWS = 275,
+  HASHFUNCTION = 274,
-     TRUSTED = 276
+  KNOWS = 275,
-   };
+  TRUSTED = 276
+};
 #endif
 /* Tokens.  */
 #define ID 258
@@ -74,22 +85,21 @@
 
 
 
-#if ! defined (YYSTYPE) && ! defined (YYSTYPE_IS_DECLARED)
+#if ! defined YYSTYPE && ! defined YYSTYPE_IS_DECLARED
+typedef union YYSTYPE
 #line 13 "parser.y"
-typedef union YYSTYPE {
+{
-	char*  		str;
+  char *str;
-	struct tacnode*	tac;
+  struct tacnode *tac;
-	Symbol		symb;
+  Symbol symb;
-	int		value;
+  int value;
-} YYSTYPE;
+}
-/* Line 1447 of yacc.c.  */
+/* Line 1529 of yacc.c.  */
-#line 87 "parser.h"
+#line 98 "parser.h"
-# define yystype YYSTYPE /* obsolescent; will be withdrawn */
+YYSTYPE;
+# define yystype YYSTYPE	/* obsolescent; will be withdrawn */
 # define YYSTYPE_IS_DECLARED 1
 # define YYSTYPE_IS_TRIVIAL 1
 #endif
 
 extern YYSTYPE yylval;
-
-
-

src/term.c

@@ -315,7 +315,7 @@ termInTerm (Term t, Term tsub)
 void
 termPrintCustom (Term term, char *leftvar, char *rightvar, char *lefttup,
 		 char *righttup, char *leftenc, char *rightenc,
-		 void (*callback) (int rid))
+		 void (*callback) (const Term t))
 {
 #ifdef DEBUG
   if (!DEBUGL (4))
@@ -345,7 +345,7 @@ termPrintCustom (Term term, char *leftvar, char *rightvar, char *lefttup,
 	    }
 	  else
 	    {
-	      callback (TermRunid (term));
+	      callback (term);
 	    }
 	}
       if (term->subst != NULL)
@@ -404,7 +404,7 @@ termPrint (Term term)
 void
 termTuplePrintCustom (Term term, char *leftvar, char *rightvar, char *lefttup,
 		      char *righttup, char *leftenc, char *rightenc,
-		      void (*callback) (int rid))
+		      void (*callback) (const Term t))
 {
   if (term == NULL)
     {

src/term.h

@@ -174,11 +174,11 @@ int termSubTerm (Term t, Term tsub);
 int termInTerm (Term t, Term tsub);
 void termPrintCustom (Term term, char *leftvar, char *rightvar, char *lefttup,
 		      char *righttup, char *leftenc, char *rightenc,
-		      void (*callback) (int rid));
+		      void (*callback) (const Term t));
 void termPrint (Term term);
 void termTuplePrintCustom (Term term, char *leftvar, char *rightvar,
 			   char *lefttup, char *righttup, char *leftenc,
-			   char *rightenc, void (*callback) (int rid));
+			   char *rightenc, void (*callback) (const Term t));
 void termTuplePrint (Term term);
 Term termDuplicate (const Term term);
 Term termNodeDuplicate (const Term term);