- Implemented --check=Secret switch, which allows checking of specific

properties.
- Fixed a bug in the symbol table, where symbols were never inserted
  into the hash table.

src/compiler.c

@@ -18,6 +18,7 @@
 */
 
 static System sys;
+static Tac tac_root;
 
 /*
    Forward declarations.
@@ -67,20 +68,12 @@ static int maxruns;
 static Protocol thisProtocol;
 static Role thisRole;
 
-/* ------------------------------------------------------------------- */
-
-//! Compile the tac into the system
-/**
- *@todo Currently, the semantics assume all labels are globally unique, but this is not enforced yet. There should be some automatic renaming when compositing protocols.
- *\sa oki_nisynch
- */
+//! Init terms and such
 void
-compile (const System mysys, Tac tc, int maxrunsset)
+compilerInit (const System mysys)
 {
   int i;
 
-  /* Init globals */
-  maxruns = maxrunsset;
   /* transfer to global static variable */
   sys = mysys;
   /* init levels */
@@ -105,9 +98,30 @@ compile (const System mysys, Tac tc, int maxrunsset)
   langcons (CLAIM_Secret, "Secret", TERM_Claim);
   langcons (CLAIM_Nisynch, "Nisynch", TERM_Claim);
   langcons (CLAIM_Niagree, "Niagree", TERM_Claim);
+}
 
+//! Clean up afterwards
+void
+compilerDone (void)
+{
+  return;
+}
+
+/* ------------------------------------------------------------------- */
+
+//! Compile the tac into the system
+/**
+ *@todo Currently, the semantics assume all labels are globally unique, but this is not enforced yet. There should be some automatic renaming when compositing protocols.
+ *\sa oki_nisynch
+ */
+void
+compile (Tac tc, int maxrunsset)
+{
+  /* Init globals */
+  maxruns = maxrunsset;
+  tac_root = tc;
   /* process the tac */
-  tacProcess (tc);
+  tacProcess (tac_root);
 
   /* cleanup */
   levelDone ();
@@ -228,6 +242,12 @@ symbolFind (Symbol s)
   return NULL;
 }
 
+//! Yield a basic global constant term (we suppose it exists) or NULL, given a string
+Term findGlobalConstant (const char *s)
+{
+  return levelFind (lookup (s), 0);
+}
+
 void
 defineUsertype (Tac tcdu)
 {
@@ -372,6 +392,15 @@ commEvent (int event, Tac tc)
       /* check for several types */
       claim = tupleProject (claimbig, 0);
       torole = claim;
+
+      /* check for ignored claim types */
+      if (sys->switchClaimToCheck != NULL &&
+	  sys->switchClaimToCheck != claim)
+	{
+	  /* abort the construction of the node */
+	  return;
+	}
+
       /* check for obvious flaws */
       if (claim == NULL)
 	{

src/compiler.h

@@ -1,7 +1,11 @@
 #ifndef COMPILER
 #define COMPILER
 
-void compile (const System sys, Tac tc, int maxruns);
+void compilerInit (const System sys);
+void compilerDone (void);
+
+void compile (Tac tc, int maxruns);
 void preprocess (const System sys);
+Term findGlobalConstant (const char *s);
 
 #endif

src/main.c

@@ -57,6 +57,7 @@
 #include "argtable2.h"
 
 extern struct tacnode *spdltac;
+extern Term TERM_Claim;
 void scanner_cleanup (void);
 void strings_cleanup (void);
 int yyparse (void);
@@ -83,6 +84,7 @@ main (int argc, char **argv)
 
   struct arg_file *infile  = arg_file0(NULL,NULL,"FILE",    "input file ('-' for stdin)");
   struct arg_file *outfile = arg_file0("o","output","FILE", "output file (default is stdout)");
+  struct arg_str *switch_check = arg_str0(NULL,"check","CLAIM","claim type to check (default is all)");
   struct arg_int *switch_scenario =
       arg_int0 ("s", "scenario", NULL, "select a scenario instance 1-n (-1 to count)");
   struct arg_int *switch_scenario_size =
@@ -140,6 +142,7 @@ main (int argc, char **argv)
     switch_echo,
     switch_progress_bar, 
 
+    switch_check,
     switch_traversal_method, 
     switch_match_method, 
     switch_clp,
@@ -300,6 +303,8 @@ main (int argc, char **argv)
    */
 
   sys = systemInit ();
+  /* init compiler for this system */
+  compilerInit (sys);
 
   /* transfer command line */
   sys->argc = argc;
@@ -369,6 +374,31 @@ main (int argc, char **argv)
   sys->latex = switch_latex_output->count;
   sys->know = emptyKnowledge ();
 
+
+  /* parse compiler-dependant switches */
+  if (switch_check->count > 0)
+    {
+      Term claim;
+
+#ifdef DEBUG
+      if (lookup(switch_check->sval[0]) == NULL)
+	{
+	  globalError++;
+	  warning ("Could not find this string at all in:");
+	  symbolPrintAll ();
+	  eprintf ("\n");
+	  globalError--;
+	}
+#endif
+      claim = findGlobalConstant (switch_check->sval[0]);
+      if (claim == NULL)
+	  error ("Unknown claim type to check.");
+      if (inTermlist (claim->stype, TERM_Claim))
+	  sys->switchClaimToCheck = claim;
+      else
+	  error ("Claim type to check is not a claim.");
+    }
+
   /* parse input */
 
   yyparse ();
@@ -379,7 +409,7 @@ main (int argc, char **argv)
 
   /* compile */
 
-  compile (sys, spdltac, switch_maximum_runs->ival[0]);
+  compile (spdltac, switch_maximum_runs->ival[0]);
   scanner_cleanup ();
 
   /* preprocess */
@@ -548,6 +578,7 @@ main (int argc, char **argv)
 
   knowledgeDestroy (sys->know);
   systemDone (sys);
+  compilerDone ();
 
   /* done symbols */
   tacDone ();

src/modelchecker.c

@@ -1037,6 +1037,7 @@ traversePOR8 (const System sys)
 //! Check for the properties that have lasting effects throughout the trace.
 /**
  * Currently, only functions for secrecy.
+ *@returns 1 (true) iff everything is okay, and no attack is found. 0 (false) if an attack is found.
  */
 
 int

src/symbol.c

@@ -84,7 +84,7 @@ get_symb (void)
 
 //! Declare a symbol to be freed.
 void
-free_symb (Symbol s)
+free_symb (const Symbol s)
 {
   if (s == NULL)
     return;
@@ -94,7 +94,7 @@ free_symb (Symbol s)
 
 //! Return the index in the hash table for the string.
 int
-hash (char *s)
+hash (const char *s)
 {
   int hv = 0;
   int i;
@@ -110,7 +110,7 @@ hash (char *s)
 
 //! Insert a string into the hash table.
 void
-insert (Symbol s)
+insert (const Symbol s)
 {
   int hv;
 
@@ -124,7 +124,7 @@ insert (Symbol s)
 
 //! Find a string in the hash table.
 Symbol
-lookup (char *s)
+lookup (const char *s)
 {
   int hv;
   Symbol t;
@@ -147,7 +147,7 @@ lookup (char *s)
 
 //! Print a symbol.
 void
-symbolPrint (Symbol s)
+symbolPrint (const Symbol s)
 {
   if (s == NULL)
     return;
@@ -156,13 +156,41 @@ symbolPrint (Symbol s)
   eprintf ("%s", s->text);
 }
 
+//! Print all symbols
+void
+symbolPrintAll (void)
+{
+  int i, count;
+
+  eprintf ("List of all symbols\n");
+  count = 0;
+  for (i = 0; i < HASHSIZE; i++)
+    {
+      Symbol sym;
+
+      sym = symbtab[i];
+      if (sym != NULL)
+	{
+	  eprintf ("H%i:\t", i);
+	  while (sym != NULL)
+	    {
+	      count++;
+	      eprintf ("[%s]\t", sym->text);
+	      sym = sym->next;
+	    }
+	  eprintf ("\n");
+	}
+    }
+  eprintf ("Total:\t%i\n", count);
+}
+
 //! Insert a string into the symbol table, if it wasn't there yet.
 /**
  * Also sets line numbers and type.
  *\sa T_SYSCONST
  */
 Symbol
-symbolSysConst (char *str)
+symbolSysConst (const char *str)
 {
   Symbol symb;
 
@@ -173,6 +201,7 @@ symbolSysConst (char *str)
       symb->lineno = yylineno;
       symb->type = T_SYSCONST;
       symb->text = str;
+      insert (symb);
     }
   return symb;
 }

src/symbol.h

@@ -20,7 +20,7 @@ struct symbol
   //! Line number at which it occurred.
   int lineno;
   //! Ascii string with name of the symbol.
-  char *text;
+  const char *text;
   //! Possible next pointer.
   struct symbol *next;
   //! Used for linking all symbol blocks, freed or in use.
@@ -33,12 +33,13 @@ void symbolsInit (void);
 void symbolsDone (void);
 
 Symbol get_symb (void);
-void free_symb (Symbol s);
+void free_symb (const Symbol s);
 
-void insert (Symbol s);
-Symbol lookup (char *s);
-void symbolPrint (Symbol s);
-Symbol symbolSysConst (char *str);
+void insert (const Symbol s);
+Symbol lookup (const char *s);
+void symbolPrint (const Symbol s);
+void symbolPrintAll (void);
+Symbol symbolSysConst (const char *str);
 
 void eprintf (char *fmt, ... );
 

src/system.c

@@ -67,6 +67,7 @@ systemInit ()
   sys->switchNomoreClaims = 1;	// default cutter when there are no more claims
   sys->switchReduceEndgame = 1;	// default cutter of last events in a trace
   sys->switchClaims = 0;	// default don't report on claims
+  sys->switchClaimToCheck = NULL;	// default check all claims
 
   /* set illegal traversal by default, to make sure it is set
      later */

src/system.h

@@ -130,6 +130,7 @@ struct system
   int switchNomoreClaims;	//!< Enable no more claims cutter
   int switchReduceEndgame;	//!< Enable endgame cutter
   int switchClaims;		//!< Enable clails report
+  Term switchClaimToCheck;	//!< Which claim should be checked?
 
   //! Latex output switch.
   /**

src/term.c

@@ -832,9 +832,9 @@ int termOrder (Term t1, Term t2)
       /* compare names */
       int comp;
 
-      name1 = t1->left.symb->text;
-      name2 = t2->left.symb->text;
-      comp = strcmp (name1,name2);
+      comp = strcmp (t1->left.symb->text,
+      		     t2->left.symb->text
+		     );
       if (comp != 0)
 	{
 	  /* names differ */

src/todo.txt

@@ -7,8 +7,6 @@
 - Intruder should at least have one copy of each type that an agent can
   construct, I think in any case. Proof needed for single identifier need.
   Furthermore reduction if type flaw testing; only one constant needed.
-- Make filter switch, allowing maybe for some claims only to be evaluated.
-  --check=Secret, --check-all as default.
 - Make --with-argtabledir= something switch, replacing
   README/galious-configure.sh constructs.
 - Move initial intruder knowledge maybe into the title of the MSC.