From 6c4b8fbc9a95f9ce336f5cd2fb0ac6f4a09313c5 Mon Sep 17 00:00:00 2001 From: ccremers Date: Fri, 14 May 2004 17:29:26 +0000 Subject: [PATCH] - Added already quite some documentation. --- src/latex.c | 154 ++++++++++++++++++++-------------------------------- src/main.c | 25 +++++++-- 2 files changed, 79 insertions(+), 100 deletions(-) diff --git a/src/latex.c b/src/latex.c index 51b7ee4..2651025 100644 --- a/src/latex.c +++ b/src/latex.c @@ -13,7 +13,9 @@ #include "varbuf.h" #include "output.h" +//! Multiplication factor for distance between events in an MSC diagram. #define EVENTSPACE 1 +//! Similarity factor required for connecting arrows. Ranges from 0 to 1. #define LINKTHRESHOLD 0.95 extern const char *progname; @@ -21,8 +23,7 @@ extern const char *releasetag; extern int globalLatex; extern Term TERM_Function; -/* struct for additional info */ - +/*! Additional information for an events. */ struct traceinfo { int match; @@ -31,14 +32,30 @@ struct traceinfo /* global variables for this module */ +//! Additional information for each event in the trace. struct traceinfo *tinfo; +//! The maximum run number involved, plus 1. int width; +//! Landscape/portrait switch. Currently not used. int landscape = 0; -int *runPerm; + +//! Phase of MSC production. +/** + * In pass 1, the widths of the boxes are determined. + * In pass 2 the actual MSC is constructed. + */ int pass; /* code */ +//! Start the latex output. +/** Prints some headers, and + * the command line that was used, as comments. + *@param sys The system buffer. + *@param argv The command line arguments as they were passed to the tool. + *@param argc The number of arguments. + */ + void latexInit (const System sys, int argc, char **argv) { @@ -60,21 +77,23 @@ latexInit (const System sys, int argc, char **argv) printf ("\\newcommand{\\comment}[1]{}\n"); } +//! Close up any LaTeX output. +/** + *@param sys The system state. + */ + void latexDone (const System sys) { /* closing of the document */ } -/* - * latexTermPrint - * - * basically a recode of termPrint, now specific using latex codes and with a +//! Print a term using LaTeX and highlighting. +/** + * Basically a recode of termPrint, now specific using latex codes and with a * highlighting feature. - * - * In: - * - a term to be printed. - * - a list of terms to be highlighted. + *@param term a term to be printed. + *@param highlight a list of terms to be highlighted. */ void @@ -150,9 +169,12 @@ latexTermPrint (Term term, Termlist highlight) } } -/* - * extending LaTeX term printing to term list printing, again with highlight +//! Print a termlist in LaTeX using highlighting. +/** + * Extending LaTeX term printing to term list printing, again with highlight * list parameter. + *@param tl A term list to print. + *@param highlight Any terms to be highlighted. */ void @@ -172,9 +194,7 @@ latexTermlistPrint (Termlist tl, Termlist highlight) } } -/* - * Display the timers and states traversed, LaTeX version. - */ +//! Display the timers and states traversed using LaTeX. void latexTimers (const System sys) @@ -246,10 +266,10 @@ latexTimers (const System sys) printf ("\\end{tabular}\n\n"); } -/* - * Start drawing MSC environment. - * - * Includes printing title +//! Start drawing MSC environment. +/** + * Includes printing title. + *@param protocolnames A termlist with protocol name terms. */ void @@ -263,9 +283,7 @@ latexMSCStart (Termlist protocolnames) printf ("$}\n"); } -/* - * Close drawing MSC - */ +//! Close drawing MSC void latexMSCEnd () @@ -277,11 +295,12 @@ latexMSCEnd () } -/* +/** * Declare the MSC stick for a single instance of a run participating in an * attack. - * * This involves layout of the partners roles, and the agent etc. + *@param sys System state. + *@param run The run to be declared. */ void @@ -338,10 +357,11 @@ latexDeclInst (const System sys, int run) termDelete (myAgent); } -/* +//! Add vertical space in MSC diagrams. +/** * Make some space in the diagram by nextlevels. - * * TODO: can be incorporated in nextlevel[param] without loop. + *@param amount the line integer. */ void @@ -359,7 +379,8 @@ latexEventSpace (int amount) printf ("\\nextlevel\n"); } -/* +//! MSC message print. +/** * Print an arrow with message from event i to event j, as defined in the * tracebuffer. If either i or j are -1, the intruder is meant. */ @@ -425,7 +446,7 @@ latexMessagePrint (struct tracebuf *tb, int from, int to) } } -/* +/** * hmm? TODO apparently, some other variant used, with duplicate handling of * lost and found ??? But only using lost... weirdness. */ @@ -490,23 +511,9 @@ latexMessagePrintHighlight (struct tracebuf *tb, int from, int to, } } -/* - * ?? TODO - */ - -void -latexAction (struct tracebuf *tb, int te) -{ - printf ("\\action{$"); - termPrint (tb->event[te]->message); - printf ("$}{run%d}\n", tb->run[te]); - //printf("\\nextlevel\n"); -} - -/* - * display claim violation. - * - * for now, only secrecy: TODO +//! Display claim violation. +/** + * For now, only secrecy: TODO */ void @@ -533,9 +540,10 @@ latexClaim (struct tracebuf *tb, int run, Termlist tl) } } -/* +//! Determine matching send event. +/** * Given a read event, tries to find a corresponding send event in the trace - * buffer. + * buffer. Currently unused. */ int @@ -643,47 +651,9 @@ latexCorrespondingSend (struct tracebuf *tb, int rd) return bestSendEvent; } -/* - * VERY broken. Mindwipe and recursion using inKnowledge, so this can't work. - * - * Apparently, it's supposed to find any subterm and was added in revision 526 - * by Lutger. - */ - -int -newInKnowledge (const Knowledge know, Term term) -{ - /* if there is no term, then it's okay 'fur sure' */ - if (term == NULL) - return 1; - /* if there is a term, but no knowledge, we're in trouble */ - if (know == NULL) - return 0; - - mindwipe (know, inKnowledge (know, term)); - - term = deVar (term); - if (isTermLeaf (term)) - { - return inTermlist (know->basic, term); - } - if (term->type == ENCRYPT) - { - return inTermlist (know->encrypt, term) || - (inKnowledge (know, term->key) || inKnowledge (know, term->op)); - } - if (term->type == TUPLE) - { - return (inTermlist (know->encrypt, term) || - (inKnowledge (know, term->op1) || - inKnowledge (know, term->op2))); - } - return 0; /* unrecognized term type, weird */ -} - -/* +//! Determine matching send event. +/** * Simplified variant of finding the matching send event. - * * However, if it is introduced at a non-send event, things start to break * done. REVIEW later. */ @@ -713,9 +683,7 @@ latexCorrespondingSend2 (struct tracebuf *tb, int readEvent) } -/* - * Display knowledge in LaTeX format. - */ +//! Display knowledge in LaTeX. void knowledgePrintLatex (Knowledge know) @@ -734,9 +702,7 @@ knowledgePrintLatex (Knowledge know) } } -/* - * Display an attack - */ +//! Display the attack in the systems attack buffer using LaTeX. void attackDisplayLatex (System sys) diff --git a/src/main.c b/src/main.c index 88780d5..d7edb16 100644 --- a/src/main.c +++ b/src/main.c @@ -27,9 +27,12 @@ void MC_incTraces (const System sys); void MC_single (const System sys); int modelCheck (const System sys); +//! The name of this program. const char *progname = "scyther"; +//! Release tag name. const char *releasetag = "alpha2-devel"; +//! The main body, as called by the environment. int main (int argc, char **argv) { @@ -365,6 +368,11 @@ exit: return exitcode; } +//! Display time and state space size information using ASCII. +/** + * Displays also whether an attack was found or not. + */ + void timersPrint (const System sys) { @@ -425,9 +433,8 @@ timersPrint (const System sys) printf ("\n"); } +//! Analyse the model by incremental runs. /* - * Analyse the model. - * * This procedure considers mainly incremental searches, and settings * parameters for that. The real work is handled by modelCheck. */ @@ -468,6 +475,12 @@ MC_incRuns (const System sys) while (flag && runs <= maxruns); } +//! Analyse the model by incremental trace lengths. +/* + * This procedure considers mainly incremental searches, and settings + * parameters for that. The real work is handled by modelCheck. + */ + void MC_incTraces (const System sys) { @@ -513,8 +526,9 @@ MC_incTraces (const System sys) while (flag && tracelen <= maxtracelen); } -/* - * Traditional handywork +//! Analyse the model with a fixed scenario. +/** + * Traditional handywork. */ void @@ -528,9 +542,8 @@ MC_single (const System sys) modelCheck (sys); } +//! Model check the system, given all parameters. /* - * Model check the system, given all parameters. - * * Precondition: the system was reset with the corresponding parameters. * This also reports on time and states traversed. */