- Made all references to system explicit const references.
- Removed config.h reference.
This commit is contained in:
parent
2065c89add
commit
b570ca2d8a
@ -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;
|
||||
|
@ -1 +1 @@
|
||||
void attackMinimize(System sys, struct tracebuf *tb);
|
||||
void attackMinimize(const System sys, struct tracebuf *tb);
|
||||
|
@ -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;
|
||||
|
||||
|
@ -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
|
||||
|
@ -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);
|
||||
|
@ -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;
|
||||
|
@ -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);
|
||||
|
||||
|
@ -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;
|
||||
|
10
src/report.c
10
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)
|
||||
{
|
||||
|
@ -1,6 +1,6 @@
|
||||
#ifndef REPORT
|
||||
#define REPORT
|
||||
|
||||
void reportSecrecy (System sys, Term t);
|
||||
void reportSecrecy (const System sys, Term t);
|
||||
|
||||
#endif
|
||||
|
18
src/runs.c
18
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)
|
||||
{
|
||||
|
18
src/runs.h
18
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);
|
||||
|
@ -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)
|
||||
|
@ -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)
|
||||
|
@ -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;
|
||||
|
||||
|
@ -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
|
||||
|
Loading…
Reference in New Issue
Block a user