diff --git a/src/attackminimize.c b/src/attackminimize.c index 869a124..13ef899 100644 --- a/src/attackminimize.c +++ b/src/attackminimize.c @@ -14,7 +14,7 @@ int cTod = 0; *@param tb The attack buffer. *@param ev The reference event index. */ -void markback(System sys, struct tracebuf *tb, int ev) +void markback(const System sys, struct tracebuf *tb, int ev) { int run = tb->run[ev]; @@ -53,7 +53,7 @@ void markback(System sys, struct tracebuf *tb, int ev) } //! Minimize the attack. -void attackMinimize(System sys, struct tracebuf *tb) +void attackMinimize(const System sys, struct tracebuf *tb) { int i; int j; diff --git a/src/attackminimize.h b/src/attackminimize.h index 5d0e8f8..efca999 100644 --- a/src/attackminimize.h +++ b/src/attackminimize.h @@ -1 +1 @@ -void attackMinimize(System sys, struct tracebuf *tb); +void attackMinimize(const System sys, struct tracebuf *tb); diff --git a/src/compiler.c b/src/compiler.c index 734a108..95ebee0 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -74,7 +74,7 @@ static Role thisRole; *\sa oki_nisynch */ void -compile (System mysys, Tac tc, int maxrunsset) +compile (const System mysys, Tac tc, int maxrunsset) { int i; diff --git a/src/compiler.h b/src/compiler.h index c6e19ca..b2668aa 100644 --- a/src/compiler.h +++ b/src/compiler.h @@ -1,7 +1,7 @@ #ifndef COMPILER #define COMPILER -void compile (System sys, Tac tc, int maxruns); +void compile (const System sys, Tac tc, int maxruns); void preprocess (const System sys); #endif diff --git a/src/debug.h b/src/debug.h index c0f5278..2e3253d 100644 --- a/src/debug.h +++ b/src/debug.h @@ -1,8 +1,6 @@ #ifndef DEBUG_H #define DEBUG_H -#include "config.h" - void debugSet (int level); int debugCond (int level); void debug (int level, char *string); diff --git a/src/latex.c b/src/latex.c index 74c63e5..9e46dcc 100644 --- a/src/latex.c +++ b/src/latex.c @@ -663,7 +663,7 @@ knowledgePrintLatex (Knowledge know) //! Display the attack in the systems attack buffer using LaTeX. void -attackDisplayLatex (System sys) +attackDisplayLatex (const System sys) { int i; struct tracebuf *tb; diff --git a/src/latex.h b/src/latex.h index e447395..f9730f0 100644 --- a/src/latex.h +++ b/src/latex.h @@ -13,8 +13,8 @@ void latexTimers(const System sys); void latexMSCStart(); void latexMSCEnd(); void latexLearnComment(const System sys, Termlist tl); -void latexTracePrint(System sys); -void attackDisplayLatex(System sys); +void latexTracePrint(const System sys); +void attackDisplayLatex(const System sys); void latexTermPrint (Term term, Termlist hl); void latexTermTuplePrint (Term term, Termlist hl); diff --git a/src/output.c b/src/output.c index f5c3206..3764343 100644 --- a/src/output.c +++ b/src/output.c @@ -25,7 +25,7 @@ linePrint (int i) } int -correspondingSend (System sys, int rd) +correspondingSend (const System sys, int rd) { int labelMatch = 0; @@ -198,7 +198,7 @@ correspondingSend (System sys, int rd) } void -tracePrint (System sys) +tracePrint (const System sys) { int i, j; int lastrid; @@ -347,7 +347,7 @@ tracePrint (System sys) void -attackDisplayAscii (System sys) +attackDisplayAscii (const System sys) { int i, j; int length; @@ -479,7 +479,7 @@ attackDisplayAscii (System sys) void -attackDisplay (System sys) +attackDisplay (const System sys) { if (!sys->report || sys->switchStatespace) return; diff --git a/src/report.c b/src/report.c index 0ca4a83..c169736 100644 --- a/src/report.c +++ b/src/report.c @@ -9,7 +9,7 @@ extern int globalLatex; /* reportQuit is called after each violation, because it might need to abort the process */ void -reportQuit (System sys) +reportQuit (const System sys) { /* determine quit or not */ if (sys->prune >= 3) @@ -22,7 +22,7 @@ reportQuit (System sys) } void -reportStart (System sys) +reportStart (const System sys) { if (!sys->latex) { @@ -34,7 +34,7 @@ reportStart (System sys) } void -reportMid (System sys) +reportMid (const System sys) { indent (); printf ("Trace length %i.\n", 1 + sys->step); @@ -45,7 +45,7 @@ reportMid (System sys) void -reportEnd (System sys) +reportEnd (const System sys) { if (!sys->latex) { @@ -56,7 +56,7 @@ reportEnd (System sys) } void -reportSecrecy (System sys, Term t) +reportSecrecy (const System sys, Term t) { if (!sys->report) { diff --git a/src/report.h b/src/report.h index 27b0e8d..232ce4c 100644 --- a/src/report.h +++ b/src/report.h @@ -1,6 +1,6 @@ #ifndef REPORT #define REPORT -void reportSecrecy (System sys, Term t); +void reportSecrecy (const System sys, Term t); #endif diff --git a/src/runs.c b/src/runs.c index 74989d5..e29192d 100644 --- a/src/runs.c +++ b/src/runs.c @@ -150,7 +150,7 @@ systemReset (const System sys) *\sa systemDestroy() */ void -systemDone (System sys) +systemDone (const System sys) { int run; int s; @@ -176,7 +176,7 @@ systemDone (System sys) //! Approximate the number of states traversed using a double type. double -statesApproximation (System sys) +statesApproximation (const System sys) { if (sys->statesHigh == 0) return (double) sys->statesLow; @@ -186,14 +186,14 @@ statesApproximation (System sys) //! Print a short version of the number of states. void -statesPrintShort (System sys) +statesPrintShort (const System sys) { fprintf (stderr,"%.3e", statesApproximation (sys)); } //! Print the number of states. void -statesPrint (System sys) +statesPrint (const System sys) { if (sys->statesHigh == 0) { @@ -217,7 +217,7 @@ statesPrint (System sys) *\sa systemDone() */ void -systemDestroy (System sys) +systemDestroy (const System sys) { memFree (sys->runs, sys->maxruns * sizeof (struct run)); memFree (sys, sizeof (struct system)); @@ -230,7 +230,7 @@ systemDestroy (System sys) */ void -ensureValidRun (System sys, int run) +ensureValidRun (const System sys, int run) { int i, oldsize; @@ -336,7 +336,7 @@ runPrint (Roledef rd) //! Print all runs in the system structure. void -runsPrint (System sys) +runsPrint (const System sys) { int i; @@ -750,7 +750,7 @@ roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg, Clai */ void -systemStart (System sys) +systemStart (const System sys) { int i, s; Roledef rd; @@ -953,7 +953,7 @@ rolesPrint (Role r) *@return True iff any agent in the list is untrusted. */ int -untrustedAgent (System sys, Termlist agents) +untrustedAgent (const System sys, Termlist agents) { while (agents != NULL) { diff --git a/src/runs.h b/src/runs.h index fe5a22c..9c18c0e 100644 --- a/src/runs.h +++ b/src/runs.h @@ -268,15 +268,15 @@ typedef struct system *System; System systemInit (); void systemReset (const System sys); -System systemDuplicate (System fromsys); -void statesPrint (System sys); -void statesPrintShort (System sys); -void systemDestroy (System sys); -void systemDone (System sys); -void ensureValidRun (System sys, int run); +System systemDuplicate (const System fromsys); +void statesPrint (const System sys); +void statesPrintShort (const System sys); +void systemDestroy (const System sys); +void systemDone (const System sys); +void ensureValidRun (const System sys, int run); void roledefPrint (Roledef rd); void runPrint (Roledef rd); -void runsPrint (System sys); +void runsPrint (const System sys); Term agentOfRunRole (const System sys, const int run, const Term role); Term agentOfRun (const System sys, const int run); Roledef roledefDuplicate1 (const Roledef rd); @@ -287,7 +287,7 @@ void roleInstance (const System sys, const Protocol protocol, const Role role, const Termlist tolist); Roledef roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl); Roledef roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg, Claimlist cl); -void systemStart (System sys); +void systemStart (const System sys); void indentActivate (); void indentSet (int i); void indent (); @@ -299,7 +299,7 @@ void protocolPrint (Protocol p); void protocolsPrint (Protocol p); void rolePrint (Role r); void rolesPrint (Role r); -int untrustedAgent (System sys, Termlist agents); +int untrustedAgent (const System sys, Termlist agents); int getMaxTraceLength (const System sys); void agentsOfRunPrint (const System sys, const int run); void violatedClaimPrint (const System sys, int i); diff --git a/src/terms.c b/src/terms.c index aeca1eb..b21fc92 100644 --- a/src/terms.c +++ b/src/terms.c @@ -137,7 +137,7 @@ makeTermType (const int type, const Symbol symb, const int runid) *@return A term that is either not a variable, or has a NULL substitution. *\sa deVar() */ -Term +__inline__ Term deVarScan (Term t) { while (realTermVariable (t) && t->subst != NULL) diff --git a/src/terms.h b/src/terms.h index b571c3c..deb97e5 100644 --- a/src/terms.h +++ b/src/terms.h @@ -63,7 +63,7 @@ void termsDone (void); Term makeTermEncrypt (Term t1, Term t2); Term makeTermTuple (Term t1, Term t2); Term makeTermType (const int type, const Symbol symb, const int runid); -Term deVarScan (Term t); +__inline__ Term deVarScan (Term t); #define substVar(t) ((t != NULL && t->type == VARIABLE && t->subst != NULL) ? 1 : 0) #define deVar(t) ( substVar(t) ? deVarScan(t->subst) : t) #define realTermLeaf(t) (t != NULL && t->type <= LEAF) diff --git a/src/varbuf.c b/src/varbuf.c index bff1660..7e064a7 100644 --- a/src/varbuf.c +++ b/src/varbuf.c @@ -13,7 +13,7 @@ */ Varbuf -varbufInit (System sys) +varbufInit (const System sys) { Varbuf vb; Termlist tl; @@ -55,7 +55,7 @@ varbufInit (System sys) */ void -varbufSet (System sys, Varbuf vb) +varbufSet (const System sys, Varbuf vb) { Termlist tl1, tl2; diff --git a/src/varbuf.h b/src/varbuf.h index b68c348..6bc454d 100644 --- a/src/varbuf.h +++ b/src/varbuf.h @@ -3,8 +3,8 @@ #include "runs.h" -Varbuf varbufInit (System sys); -void varbufSet (System sys, Varbuf vb); +Varbuf varbufInit (const System sys); +void varbufSet (const System sys, Varbuf vb); void varbufDone (Varbuf vb); #endif