From b6e9841c0f6c5240c4f2cc6593a1cc7e59534caa Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 16 Jun 2005 14:10:07 +0000 Subject: [PATCH] - Moved special terms into their own (very) special file. --- src/arachne.c | 11 +--------- src/compiler.c | 46 +++------------------------------------- src/compiler.h | 8 +++++++ src/latex.c | 2 +- src/main-switches.c | 2 +- src/main.c | 3 +-- src/mgu.c | 3 +-- src/modelchecker.c | 6 +----- src/specialterm.c | 51 +++++++++++++++++++++++++++++++++++++++++++++ src/specialterm.h | 21 +++++++++++++++++++ src/switches.c | 2 +- src/system.c | 5 +---- src/term.c | 2 +- src/termlist.c | 8 +------ src/type.c | 11 +--------- src/xmlout.c | 2 +- 16 files changed, 95 insertions(+), 88 deletions(-) create mode 100644 src/specialterm.c create mode 100644 src/specialterm.h diff --git a/src/arachne.c b/src/arachne.c index 35e0f52..d726552 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -32,16 +32,7 @@ #include "timer.h" #include "type.h" #include "switches.h" - -extern Term CLAIM_Secret; -extern Term CLAIM_Nisynch; -extern Term CLAIM_Niagree; -extern Term CLAIM_Empty; - -extern Term TERM_Agent; -extern Term TERM_Hidden; -extern Term TERM_Function; -extern Term TERM_Nonce; +#include "specialterm.h" extern int *graph; extern int nodes; diff --git a/src/compiler.c b/src/compiler.c index 2e4e420..deffb1c 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -11,6 +11,7 @@ #include "substitution.h" #include "compiler.h" #include "switches.h" +#include "specialterm.h" /* Simple sys pointer as a global. Yields cleaner code although it's against programming standards. @@ -34,8 +35,6 @@ extern int protocolCount; void tacProcess (Tac tc); void levelInit (void); void levelDone (void); -Term symbolDeclare (Symbol s, int isVar); -void levelTacDeclaration (Tac tc, int isVar); Term levelFind (Symbol s, int i); Term symbolFind (Symbol s); Term tacTerm (Tac tc); @@ -43,29 +42,6 @@ Termlist tacTermlist (Tac tc); Term levelDeclare (Symbol s, int isVar, int level); void compute_role_variables (const System sys, Protocol p, Role r); -#define levelDeclareVar(s) levelTacDeclaration(s,1) -#define levelDeclareConst(s) levelTacDeclaration(s,0) -#define levelVar(s) symbolDeclare(s,1) -#define levelConst(s) symbolDeclare(s,0) - -/* externally used: - * TERM_Function in termlists.c for inversekeys - * TERM_Type in system.c for type determination. - */ - -Term TERM_Agent; -Term TERM_Function; -Term TERM_Hidden; -Term TERM_Type; -Term TERM_Nonce; -Term TERM_Ticket; - -Term TERM_Claim; -Term CLAIM_Secret; -Term CLAIM_Nisynch; -Term CLAIM_Niagree; -Term CLAIM_Empty; - /* * Global stuff */ @@ -92,24 +68,8 @@ compilerInit (const System mysys) level = -1; levelInit (); - /* Init system constants */ -#define langhide(x,y) x = levelConst(symbolSysConst(" _" y "_ ")) -#define langtype(x,y) x->stype = termlistAdd(x->stype,y); -#define langcons(x,y,z) x = levelConst(symbolSysConst(y)); langtype(x,z) - - langhide (TERM_Type, "Type"); - langhide (TERM_Hidden, "Hidden"); - langhide (TERM_Claim, "Claim"); - - langcons (TERM_Agent, "Agent", TERM_Type); - langcons (TERM_Function, "Function", TERM_Type); - langcons (TERM_Nonce, "Nonce", TERM_Type); - langcons (TERM_Ticket, "Ticket", TERM_Type); - - langcons (CLAIM_Secret, "Secret", TERM_Claim); - langcons (CLAIM_Nisynch, "Nisynch", TERM_Claim); - langcons (CLAIM_Niagree, "Niagree", TERM_Claim); - langcons (CLAIM_Empty, "Empty", TERM_Claim); + /* create special terms */ + specialTermInit (sys); } //! Make a global constant diff --git a/src/compiler.h b/src/compiler.h index 7ea6969..c6dc011 100644 --- a/src/compiler.h +++ b/src/compiler.h @@ -15,4 +15,12 @@ Term makeGlobalConstant (const char *s); Term makeGlobalVariable (const char *s); void compute_role_variables (const System sys, Protocol p, Role r); +Term symbolDeclare (Symbol s, int isVar); +void levelTacDeclaration (Tac tc, int isVar); + +#define levelDeclareVar(s) levelTacDeclaration(s,1) +#define levelDeclareConst(s) levelTacDeclaration(s,0) +#define levelVar(s) symbolDeclare(s,1) +#define levelConst(s) symbolDeclare(s,0) + #endif diff --git a/src/latex.c b/src/latex.c index 23e798b..fbada43 100644 --- a/src/latex.c +++ b/src/latex.c @@ -13,6 +13,7 @@ #include "varbuf.h" #include "output.h" #include "latex.h" +#include "specialterm.h" //! Multiplication factor for distance between events in an MSC diagram. #define EVENTSPACE 1 @@ -22,7 +23,6 @@ extern const char *progname; extern const char *releasetag; extern int globalLatex; -extern Term TERM_Function; /*! Additional information for an events. */ struct traceinfo diff --git a/src/main-switches.c b/src/main-switches.c index 952969f..da936d9 100644 --- a/src/main-switches.c +++ b/src/main-switches.c @@ -58,6 +58,7 @@ enum exittypes #include "output.h" #include "binding.h" #include "version.h" +#include "specialterm.h" #include "argtable2.h" @@ -65,7 +66,6 @@ enum exittypes System sys; extern struct tacnode *spdltac; -extern Term TERM_Claim; extern int mgu_match; void scanner_cleanup (void); diff --git a/src/main.c b/src/main.c index c1039b3..f00becc 100644 --- a/src/main.c +++ b/src/main.c @@ -59,13 +59,12 @@ enum exittypes #include "output.h" #include "binding.h" #include "switches.h" +#include "specialterm.h" // The global system state System sys; extern struct tacnode *spdltac; -extern Term TERM_Claim; -extern Term CLAIM_Empty; extern int mgu_match; void scanner_cleanup (void); diff --git a/src/mgu.c b/src/mgu.c index 2641c1a..e4d200e 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -6,6 +6,7 @@ #include "mgu.h" #include "memory.h" #include "type.h" +#include "specialterm.h" /* Most General Unifier @@ -24,8 +25,6 @@ */ static int mgu_match = 0; -extern Term TERM_Hidden; - //! Set mgu mode (basically switches.match) void setMguMode (const int match) diff --git a/src/modelchecker.c b/src/modelchecker.c index e50910b..158b71e 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -21,17 +21,13 @@ #include "attackminimize.h" #include "claim.h" #include "switches.h" +#include "specialterm.h" /* A model checker. Really. */ -extern Term CLAIM_Secret; -extern Term CLAIM_Nisynch; -extern Term CLAIM_Niagree; -extern Term CLAIM_Empty; - /* Some forward declarations. */ diff --git a/src/specialterm.c b/src/specialterm.c new file mode 100644 index 0000000..742f0c9 --- /dev/null +++ b/src/specialterm.c @@ -0,0 +1,51 @@ +#include +#include +#include "term.h" +#include "compiler.h" + +/* + * Some macros + */ +#define langhide(x,y) x = levelConst(symbolSysConst(" _" y "_ ")) +#define langtype(x,y) x->stype = termlistAdd(x->stype,y); +#define langcons(x,y,z) x = levelConst(symbolSysConst(y)); langtype(x,z) + +/* externally used: + */ + +Term TERM_Agent; +Term TERM_Function; +Term TERM_Hidden; +Term TERM_Type; +Term TERM_Nonce; +Term TERM_Ticket; + +Term TERM_Claim; +Term CLAIM_Secret; +Term CLAIM_Nisynch; +Term CLAIM_Niagree; +Term CLAIM_Empty; + +//! Init special terms +/** + * This is called by compilerInit + */ +void +specialTermInit (const System sys) +{ + /* Init system constants */ + + langhide (TERM_Type, "Type"); + langhide (TERM_Hidden, "Hidden"); + langhide (TERM_Claim, "Claim"); + + langcons (TERM_Agent, "Agent", TERM_Type); + langcons (TERM_Function, "Function", TERM_Type); + langcons (TERM_Nonce, "Nonce", TERM_Type); + langcons (TERM_Ticket, "Ticket", TERM_Type); + + langcons (CLAIM_Secret, "Secret", TERM_Claim); + langcons (CLAIM_Nisynch, "Nisynch", TERM_Claim); + langcons (CLAIM_Niagree, "Niagree", TERM_Claim); + langcons (CLAIM_Empty, "Empty", TERM_Claim); +} diff --git a/src/specialterm.h b/src/specialterm.h new file mode 100644 index 0000000..e19aab5 --- /dev/null +++ b/src/specialterm.h @@ -0,0 +1,21 @@ +#ifndef SPECIALTERM +#define SPECIALTERM + +/* + * Some declarations in spercialterm.c + */ + +extern Term TERM_Agent; +extern Term TERM_Function; +extern Term TERM_Hidden; +extern Term TERM_Type; +extern Term TERM_Nonce; +extern Term TERM_Ticket; + +extern Term TERM_Claim; +extern Term CLAIM_Secret; +extern Term CLAIM_Nisynch; +extern Term CLAIM_Niagree; +extern Term CLAIM_Empty; + +#endif diff --git a/src/switches.c b/src/switches.c index fbbefac..73f5334 100644 --- a/src/switches.c +++ b/src/switches.c @@ -11,12 +11,12 @@ #include "version.h" #include "timer.h" #include "switches.h" +#include "specialterm.h" #include struct switchdata switches; extern struct tacnode *spdltac; -extern Term TERM_Claim; const char *progname = "scyther"; const char *releasetag = SVNVERSION; diff --git a/src/system.c b/src/system.c index 62da118..d7e87d9 100644 --- a/src/system.c +++ b/src/system.c @@ -18,10 +18,7 @@ #include "mgu.h" #include "switches.h" #include "binding.h" - -/* from compiler.o */ -extern Term TERM_Type; -extern Term TERM_Agent; +#include "specialterm.h" //! Global flag that signals LaTeX output. /** diff --git a/src/term.c b/src/term.c index 73ee898..7440962 100644 --- a/src/term.c +++ b/src/term.c @@ -18,13 +18,13 @@ #include "debug.h" #include "memory.h" #include "ctype.h" +#include "specialterm.h" /* public flag */ int rolelocal_variable; /* external definitions */ -extern Term TERM_Function; extern int inTermlist (); // suppresses a warning, but at what cost? extern int globalLatex; diff --git a/src/termlist.c b/src/termlist.c index cc2a001..51aed1b 100644 --- a/src/termlist.c +++ b/src/termlist.c @@ -1,16 +1,10 @@ #include #include #include "termlist.h" +#include "specialterm.h" #include "debug.h" #include "memory.h" -/* system constants. - * declared in compiler.c - */ - -extern Term TERM_Function; -extern Term TERM_Hidden; - //! Open termlists code. void termlistsInit (void) diff --git a/src/type.c b/src/type.c index 3667ffc..ebfa10a 100644 --- a/src/type.c +++ b/src/type.c @@ -11,16 +11,7 @@ #include "system.h" #include "debug.h" #include "switches.h" - -/* - * Special term definitions from compiler.c - */ -extern Term TERM_Agent; -extern Term TERM_Function; -extern Term TERM_Hidden; -extern Term TERM_Type; -extern Term TERM_Nonce; -extern Term TERM_Ticket; +#include "specialterm.h" extern Protocol INTRUDER; diff --git a/src/xmlout.c b/src/xmlout.c index 5192e46..a589260 100644 --- a/src/xmlout.c +++ b/src/xmlout.c @@ -18,6 +18,7 @@ #include "binding.h" #include "arachne.h" // for get_semitrace_length #include "switches.h" +#include "specialterm.h" #include "xmlout.h" @@ -25,7 +26,6 @@ * Externally defined */ extern Protocol INTRUDER; // from arachne.c -extern Term TERM_Function; // from termlist.c /* * Global/static stuff.