- Some fixes after pedantic tests. What remains: (a) C++ style comments (//) and (b) nested functions.

src/Makefile

@@ -1,24 +1,307 @@
-#
+# Include the progress variables for this target.
-# Scyther makefile
+include progress.make
-#
-# Scyther really uses the scons program (http://www.scons.org/), of
-# which there is a local copy present. So this is just delegating stuff.
-#
-#
-SCONS = ./scons.py
 
-all:
+# CMAKE generated file: DO NOT EDIT!
-	${SCONS} all
+# Generated by "Unix Makefiles" Generator, CMake Version 2.4
 
-windows:
+#=============================================================================
-	${SCONS} windows
+# Set environment variables for the build.
 
-linux:
+# The shell in which to execute make rules.
-	${SCONS} linux
+SHELL = /bin/sh
 
-tags:
+# The CMake executable.
-	${SCONS} tags
+CMAKE_COMMAND = /usr/bin/cmake
 
+# The command to remove a file.
+RM = /usr/bin/cmake -E remove -f
+
+# The program to use to edit the cache.
+CMAKE_EDIT_COMMAND = /usr/bin/ccmake
+
+# The top-level source directory on which CMake was run.
+CMAKE_SOURCE_DIR = /home/cas/svn/scyther/src
+
+# The top-level build directory on which CMake was run.
+CMAKE_BINARY_DIR = /home/cas/svn/scyther/src
+
+# Default target executed when no arguments are given to make.
+default_target: all
+
+# Special rule for the target edit_cache
+edit_cache:
+	@$(CMAKE_COMMAND) -E cmake_echo_color --switch=$(COLOR) --cyan "Running CMake cache editor..."
+	/usr/bin/ccmake -H$(CMAKE_SOURCE_DIR) -B$(CMAKE_BINARY_DIR)
+
+# Special rule for the target edit_cache
+edit_cache/fast: edit_cache
+
+# Special rule for the target install
+install: preinstall
+	@$(CMAKE_COMMAND) -E cmake_echo_color --switch=$(COLOR) --cyan "Install the project..."
+	/usr/bin/cmake -P cmake_install.cmake
+
+# Special rule for the target install
+install/fast: preinstall/fast
+	@$(CMAKE_COMMAND) -E cmake_echo_color --switch=$(COLOR) --cyan "Install the project..."
+	/usr/bin/cmake -P cmake_install.cmake
+
+# Special rule for the target rebuild_cache
+rebuild_cache:
+	@$(CMAKE_COMMAND) -E cmake_echo_color --switch=$(COLOR) --cyan "Running CMake to regenerate build system..."
+	/usr/bin/cmake -H$(CMAKE_SOURCE_DIR) -B$(CMAKE_BINARY_DIR)
+
+# Special rule for the target rebuild_cache
+rebuild_cache/fast: rebuild_cache
+
+#=============================================================================
+# Special targets provided by cmake.
+
+# Suppress display of executed commands.
+$(VERBOSE).SILENT:
+
+# Disable implicit rules so canoncical targets will work.
+.SUFFIXES:
+
+.SUFFIXES: .hpux_make_needs_suffix_list
+
+# The main all target
+all: cmake_check_build_system
+	$(CMAKE_COMMAND) -E cmake_progress_start /home/cas/svn/scyther/src/CMakeFiles $(CMAKE_ALL_PROGRESS)
+	$(MAKE) -f CMakeFiles/Makefile2 all
+	$(CMAKE_COMMAND) -E cmake_progress_start /home/cas/svn/scyther/src/CMakeFiles 0
+
+# The main clean target
 clean:
-	${SCONS} -c
+	$(MAKE) -f CMakeFiles/Makefile2 clean
+
+# The main clean target
+clean/fast: clean
+
+# Prepare targets for installation.
+preinstall: all
+	$(MAKE) -f CMakeFiles/Makefile2 preinstall
+
+# Prepare targets for installation.
+preinstall/fast:
+	$(MAKE) -f CMakeFiles/Makefile2 preinstall
+
+# clear depends
+depend:
+	$(CMAKE_COMMAND) -H$(CMAKE_SOURCE_DIR) -B$(CMAKE_BINARY_DIR) --check-build-system CMakeFiles/Makefile.cmake 1
+
+#=============================================================================
+# Target rules for targets named ScytherParser
+
+# Build rule for target.
+ScytherParser: cmake_check_build_system
+	$(MAKE) -f CMakeFiles/Makefile2 ScytherParser
+
+# fast build rule for target.
+ScytherParser/fast:
+	$(MAKE) -f CMakeFiles/ScytherParser.dir/build.make CMakeFiles/ScytherParser.dir/build
+
+#=============================================================================
+# Target rules for targets named scyther-cmake
+
+# Build rule for target.
+scyther-cmake: cmake_check_build_system
+	$(MAKE) -f CMakeFiles/Makefile2 scyther-cmake
+
+# fast build rule for target.
+scyther-cmake/fast:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/build
+
+# target for object file
+arachne.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/arachne.o
+
+# target for object file
+binding.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/binding.o
+
+# target for object file
+claim.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/claim.o
+
+# target for object file
+color.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/color.o
+
+# target for object file
+compiler.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/compiler.o
+
+# target for object file
+cost.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/cost.o
+
+# target for object file
+debug.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/debug.o
+
+# target for object file
+depend.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/depend.o
+
+# target for object file
+dotout.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/dotout.o
+
+# target for object file
+error.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/error.o
+
+# target for object file
+heuristic.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/heuristic.o
+
+# target for object file
+hidelevel.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/hidelevel.o
+
+# target for object file
+intruderknowledge.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/intruderknowledge.o
+
+# target for object file
+knowledge.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/knowledge.o
+
+# target for object file
+label.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/label.o
+
+# target for object file
+list.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/list.o
+
+# target for object file
+main.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/main.o
+
+# target for object file
+mgu.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/mgu.o
+
+# target for object file
+prune_bounds.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/prune_bounds.o
+
+# target for object file
+prune_theorems.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/prune_theorems.o
+
+# target for object file
+role.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/role.o
+
+# target for object file
+specialterm.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/specialterm.o
+
+# target for object file
+states.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/states.o
+
+# target for object file
+switches.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/switches.o
+
+# target for object file
+symbol.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/symbol.o
+
+# target for object file
+system.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/system.o
+
+# target for object file
+tac.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/tac.o
+
+# target for object file
+term.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/term.o
+
+# target for object file
+termlist.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/termlist.o
+
+# target for object file
+termmap.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/termmap.o
+
+# target for object file
+timer.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/timer.o
+
+# target for object file
+type.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/type.o
+
+# target for object file
+warshall.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/warshall.o
+
+# target for object file
+xmlout.o:
+	$(MAKE) -f CMakeFiles/scyther-cmake.dir/build.make CMakeFiles/scyther-cmake.dir/xmlout.o
+
+# Help Target
+help::
+	@echo "The following are some of the valid targets for this Makefile:"
+	@echo "... all (the default if no target is provided)"
+	@echo "... clean"
+	@echo "... depend"
+	@echo "... ScytherParser"
+	@echo "... edit_cache"
+	@echo "... install"
+	@echo "... rebuild_cache"
+	@echo "... scyther-cmake"
+	@echo "... arachne.o"
+	@echo "... binding.o"
+	@echo "... claim.o"
+	@echo "... color.o"
+	@echo "... compiler.o"
+	@echo "... cost.o"
+	@echo "... debug.o"
+	@echo "... depend.o"
+	@echo "... dotout.o"
+	@echo "... error.o"
+	@echo "... heuristic.o"
+	@echo "... hidelevel.o"
+	@echo "... intruderknowledge.o"
+	@echo "... knowledge.o"
+	@echo "... label.o"
+	@echo "... list.o"
+	@echo "... main.o"
+	@echo "... mgu.o"
+	@echo "... prune_bounds.o"
+	@echo "... prune_theorems.o"
+	@echo "... role.o"
+	@echo "... specialterm.o"
+	@echo "... states.o"
+	@echo "... switches.o"
+	@echo "... symbol.o"
+	@echo "... system.o"
+	@echo "... tac.o"
+	@echo "... term.o"
+	@echo "... termlist.o"
+	@echo "... termmap.o"
+	@echo "... timer.o"
+	@echo "... type.o"
+	@echo "... warshall.o"
+	@echo "... xmlout.o"
+
+
+
+#=============================================================================
+# Special targets to cleanup operation of make.
+
+# Special rule to run CMake to check the build system integrity.
+# No rule that depends on this can have commands that come from listfiles
+# because they might be regenerated.
+cmake_check_build_system:
+	$(CMAKE_COMMAND) -H$(CMAKE_SOURCE_DIR) -B$(CMAKE_BINARY_DIR) --check-build-system CMakeFiles/Makefile.cmake 0
 

src/compiler.c

@@ -1312,14 +1312,6 @@ order_label_roles (const Claimlist cl)
   distance = 0;
   while (roles_remaining != NULL)
     {
-      distance++;
-#ifdef DEBUG
-      if (DEBUGL (4))
-	{
-	  eprintf (" %i:", distance);
-	}
-#endif
-
       int scan_label (void *data)
       {
 	Labelinfo linfo;
@@ -1362,6 +1354,13 @@ order_label_roles (const Claimlist cl)
 	return 1;
       }
 
+      distance++;
+#ifdef DEBUG
+      if (DEBUGL (4))
+	{
+	  eprintf (" %i:", distance);
+	}
+#endif
       list_iterate (sys->labellist, scan_label);
     }
   cl->roles = roles_ordered;

src/hidelevel.c

@@ -18,8 +18,6 @@ protocolHidelevel (const System sys, const Term t)
 {
   unsigned int minlevel;
 
-  minlevel = INT_MAX;
-
   int itsends (const Protocol p, const Role r)
   {
     int sends (Roledef rd)
@@ -45,6 +43,7 @@ protocolHidelevel (const System sys, const Term t)
     return true;
   }
 
+  minlevel = INT_MAX;
   iterateRoles (sys, itsends);
 
   return minlevel;

src/intruderknowledge.c

@@ -36,8 +36,6 @@ addEnumTerm (const System sys, Term t, Term actor, Termlist todo,
       if (termSubTerm (t, todo->term))
 	{
 	  // Occurs, we have to iterate
-	  fromlist = termlistPrepend (fromlist, todo->term);
-
 	  void iterateThis (Term to)
 	  {
 	    tolist = termlistPrepend (tolist, to);
@@ -47,6 +45,7 @@ addEnumTerm (const System sys, Term t, Term actor, Termlist todo,
 	    tolist = termlistDelTerm (tolist);
 	  }
 
+	  fromlist = termlistPrepend (fromlist, todo->term);
 	  if (isTermEqual (todo->term, actor))
 	    {
 	      // Untrusted agents only
@@ -95,19 +94,6 @@ anySubTerm (Term t, Termlist sublist)
 void
 initialIntruderKnowledge (const System sys)
 {
-  if (switches.check)
-    {
-      globalError++;
-      eprintf ("Computing initial intruder knowledge.\n\n");
-      eprintf ("Agent names      : ");
-      termlistPrint (sys->agentnames);
-      eprintf ("\n");
-      eprintf ("Untrusted agents : ");
-      termlistPrint (sys->untrusted);
-      eprintf ("\n");
-      globalError--;
-    }
-
   /*
    * display initial role knowledge
    */
@@ -190,10 +176,22 @@ initialIntruderKnowledge (const System sys)
 	eprintf ("\n");
 	globalError--;
       }
-
     addListKnowledge (r->knows, r->nameterm);
     return true;
   }
 
+  if (switches.check)
+    {
+      globalError++;
+      eprintf ("Computing initial intruder knowledge.\n\n");
+      eprintf ("Agent names      : ");
+      termlistPrint (sys->agentnames);
+      eprintf ("\n");
+      eprintf ("Untrusted agents : ");
+      termlistPrint (sys->untrusted);
+      eprintf ("\n");
+      globalError--;
+    }
+
   iterateRoles (sys, deriveFromRole);
 }

src/mgu.c

@@ -123,14 +123,6 @@ termlistSubstReset (Termlist tl)
 int
 unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist))
 {
-  /* added for speed */
-  t1 = deVar (t1);
-  t2 = deVar (t2);
-  if (t1 == t2)
-    {
-      return callback (tl);
-    }
-
   int callsubst (Termlist tl, Term t, Term tsubst)
   {
     int proceed;
@@ -146,6 +138,14 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist))
     return proceed;
   }
 
+  /* added for speed */
+  t1 = deVar (t1);
+  t2 = deVar (t2);
+  if (t1 == t2)
+    {
+      return callback (tl);
+    }
+
   if (!(hasTermVariable (t1) || hasTermVariable (t2)))
     {
       // None has a variable

src/symbol.c

@@ -237,6 +237,9 @@ symbolNextFree (Symbol prefixsymbol)
   n = 1;
   while (n <= 9999)
     {
+      /*
+       * The construction below (variable buffer length) is not allowed in ISO C90
+       */
       char buffer[len + 5];	// thus we must enforce a maximum of 9.999 (allowing for storage of \0 )
       Symbol symb;
       int slen;

src/system.c

@@ -596,29 +596,6 @@ roleInstanceArachne (const System sys, const Protocol protocol,
   Termlist tolist = NULL;	// -> .locals
   Term extterm = NULL;		// construction thing (will go to artefacts)
 
-  /* claim runid, allocate space */
-  rid = sys->maxruns;
-  ensureValidRun (sys, rid);	// creates a new block
-  runs = sys->runs;		// simple structure pointer transfer (shortcut)
-
-  /* duplicate roledef in buffer rd */
-  /* Notice that it is not stored (yet) in the run structure,
-   * and that termDuplicate is used internally
-   */
-  rd = roledefDuplicate (role->roledef);
-
-  /* set parameters */
-  /* generic setup of inherited stuff */
-  runs[rid].protocol = protocol;
-  runs[rid].role = role;
-  runs[rid].step = 0;
-  runs[rid].firstReal = 0;
-
-  /* Now we need to create local terms corresponding to rho, sigma, and any local constants.
-   *
-   * We maintain our stuff in a from/to list.
-   */
-
   void createLocal (Term oldt, int isvariable, int isrole)
   {
     Term newt;
@@ -699,6 +676,29 @@ roleInstanceArachne (const System sys, const Protocol protocol,
       }
   }
 
+  /* claim runid, allocate space */
+  rid = sys->maxruns;
+  ensureValidRun (sys, rid);	// creates a new block
+  runs = sys->runs;		// simple structure pointer transfer (shortcut)
+
+  /* duplicate roledef in buffer rd */
+  /* Notice that it is not stored (yet) in the run structure,
+   * and that termDuplicate is used internally
+   */
+  rd = roledefDuplicate (role->roledef);
+
+  /* set parameters */
+  /* generic setup of inherited stuff */
+  runs[rid].protocol = protocol;
+  runs[rid].role = role;
+  runs[rid].step = 0;
+  runs[rid].firstReal = 0;
+
+  /* Now we need to create local terms corresponding to rho, sigma, and any local constants.
+   *
+   * We maintain our stuff in a from/to list.
+   */
+
   // Create rho, sigma, constants
   createLocals (protocol->rolenames, true, true);
   createLocals (role->declaredvars, true, false);

src/term.c

@@ -1273,9 +1273,6 @@ term_set_keylevels (const Term term)
 void
 termPrintDiff (Term t1, Term t2)
 {
-  t1 = deVar (t1);
-  t2 = deVar (t2);
-
   void termFromTo (Term t1, Term t2)
   {
     t1 = deVar (t1);
@@ -1288,6 +1285,9 @@ termPrintDiff (Term t1, Term t2)
     eprintf ("] ");
   }
 
+  t1 = deVar (t1);
+  t2 = deVar (t2);
+
   if (isTermEqual (t1, t2))
     {
       // Equal, simply print