From 080d19a8408cdcf5d919c0ee41734c353c9bb239 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Sat, 15 May 2004 16:43:20 +0000
Subject: [PATCH] - Even more documentation.

---
 src/attackminimize.c |  9 +++++++++
 src/main.c           |  4 ++++
 src/memory.c         | 13 +++++++++++++
 src/mgu.c            | 10 ++++++++++
 src/mgu.h            |  7 +++++++
 src/termlists.c      |  2 +-
 6 files changed, 44 insertions(+), 1 deletion(-)

diff --git a/src/attackminimize.c b/src/attackminimize.c
index 220dc32..869a124 100644
--- a/src/attackminimize.c
+++ b/src/attackminimize.c
@@ -3,9 +3,17 @@
 #include "runs.h"
 #include "tracebuf.h"
 
+//! Help counter for the number of unknowns.
 int cUnk = 0;
+//! Help counter for the number of todos.
 int cTod = 0;
 
+//! Mark all events of the same run before the event as required.
+/**
+ *@param sys The system.
+ *@param tb The attack buffer.
+ *@param ev The reference event index.
+ */
 void markback(System sys, struct tracebuf *tb, int ev)
 {
 	int run = tb->run[ev];
@@ -44,6 +52,7 @@ void markback(System sys, struct tracebuf *tb, int ev)
 	}
 }
 
+//! Minimize the attack.
 void attackMinimize(System sys, struct tracebuf *tb)
 {
 	int i;
diff --git a/src/main.c b/src/main.c
index a2cf6e3..ae2e6e4 100644
--- a/src/main.c
+++ b/src/main.c
@@ -57,6 +57,10 @@ int modelCheck (const System sys);
 //! The name of this program.
 const char *progname = "scyther";
 //! Release tag name.
+/**
+ * Note that this is only referenced in the help output of the commandline program.
+ * \todo Come up with a useful solution for release names.
+ */
 const char *releasetag = "alpha2-devel";
 
 //! The main body, as called by the environment.
diff --git a/src/memory.c b/src/memory.c
index 9a8881d..5955020 100644
--- a/src/memory.c
+++ b/src/memory.c
@@ -1,3 +1,14 @@
+/**
+ *@file
+ * \brief Memory functions
+ *
+ * These are not really used anymore, so maybe they should be removed.
+ * 
+ * \par Performance
+ * Tests showed that memory pooling was actually much less efficient than
+ * having \c malloc() trying to fit stuff into the memory caches.
+ */
+
 /* my own memory functions (not yet) */
 
 #include <stdlib.h>
@@ -15,6 +26,7 @@
 #include "substitutions.h"
 #include "runs.h"
 
+//! Open memory code.
 void
 memInit ()
 {
@@ -41,6 +53,7 @@ memInit ()
   return;
 }
 
+//! Close memory code.
 void
 memDone (int sw)
 {
diff --git a/src/mgu.c b/src/mgu.c
index b7b67f4..f1959b9 100644
--- a/src/mgu.c
+++ b/src/mgu.c
@@ -14,6 +14,10 @@
    New version yields a termlist with substituted variables, which can later be reset to NULL.
 */
 
+//! Undo all substitutions in a list of variables.
+/**
+ * The termlist should contain only variables.
+ */
 void
 termlistSubstReset (Termlist tl)
 {
@@ -24,6 +28,12 @@ termlistSubstReset (Termlist tl)
     }
 }
 
+//! Most general unifier.
+/**
+ * Try to determine the most general unifier of two terms.
+ *@return Returns a list of variables, that were previously open, but are now closed
+ * in such a way that the two terms unify. Returns \ref MGUFAIL if it is impossible.
+ */
 Termlist
 termMguTerm (Term t1, Term t2)
 {
diff --git a/src/mgu.h b/src/mgu.h
index e278723..5b65eef 100644
--- a/src/mgu.h
+++ b/src/mgu.h
@@ -5,6 +5,13 @@
 #include "termlists.h"
 #include "substitutions.h"
 
+//! A special constant do denote failure.
+/**
+ * \c NULL already denotes equality, so an extra signal is needed to
+ * denote that a unification fails.
+ * \todo Find a portable solution for this \c MGUFAIL constant:
+ * maybe a pointer to some special constant.
+ */
 #define MGUFAIL (Termlist) -1
 
 Termlist termMguTerm (Term t1, Term t2);
diff --git a/src/termlists.c b/src/termlists.c
index c36df18..9b92442 100644
--- a/src/termlists.c
+++ b/src/termlists.c
@@ -134,7 +134,7 @@ inTermlist (Termlist tl, Term term)
 /**
  * Are all elements of list 1 in list 2, and vice versa? 
  * Note that we assume unique elements!
- *@param True iff every element of the list is in the other list.
+ *@return True iff every element of the list is in the other list.
  */
 
 int