Removing two last nested functions.
I missed these before since they didn't seem to generate trampolines.
This commit is contained in:
parent
6f881d0b54
commit
16c149e6a2
@ -94,31 +94,33 @@ int iterate ();
|
|||||||
* Program code
|
* Program code
|
||||||
*/
|
*/
|
||||||
|
|
||||||
//! Init Arachne engine
|
//! Two simple helpers for arachneInit
|
||||||
void
|
Roledef
|
||||||
arachneInit (const System mysys)
|
add_event (Roledef rd, int event, Term message)
|
||||||
{
|
{
|
||||||
Roledef rd;
|
return roledefAdd (rd, event, NULL, NULL, NULL, message, NULL);
|
||||||
|
}
|
||||||
|
|
||||||
void add_event (int event, Term message)
|
Role
|
||||||
{
|
add_role (Roledef rd, const char *rolenamestring)
|
||||||
rd = roledefAdd (rd, event, NULL, NULL, NULL, message, NULL);
|
{
|
||||||
}
|
|
||||||
|
|
||||||
Role add_role (const char *rolenamestring)
|
|
||||||
{
|
|
||||||
Role r;
|
Role r;
|
||||||
Term rolename;
|
Term rolename;
|
||||||
|
|
||||||
rolename = makeGlobalConstant (rolenamestring);
|
rolename = makeGlobalConstant (rolenamestring);
|
||||||
r = roleCreate (rolename);
|
r = roleCreate (rolename);
|
||||||
r->roledef = rd;
|
r->roledef = rd;
|
||||||
rd = NULL;
|
|
||||||
r->next = INTRUDER->roles;
|
r->next = INTRUDER->roles;
|
||||||
INTRUDER->roles = r;
|
INTRUDER->roles = r;
|
||||||
// compute_role_variables (sys, INTRUDER, r);
|
// compute_role_variables (sys, INTRUDER, r);
|
||||||
return r;
|
return r;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
//! Init Arachne engine
|
||||||
|
void
|
||||||
|
arachneInit (const System mysys)
|
||||||
|
{
|
||||||
|
Roledef rd;
|
||||||
|
|
||||||
sys = mysys; // make sys available for this module as a global
|
sys = mysys; // make sys available for this module as a global
|
||||||
|
|
||||||
@ -133,21 +135,21 @@ arachneInit (const System mysys)
|
|||||||
|
|
||||||
INTRUDER = protocolCreate (makeGlobalConstant (" INTRUDER "));
|
INTRUDER = protocolCreate (makeGlobalConstant (" INTRUDER "));
|
||||||
|
|
||||||
// Initially empty roledef
|
|
||||||
rd = NULL;
|
rd = NULL;
|
||||||
|
rd = add_event (rd, SEND, NULL);
|
||||||
|
I_M = add_role (rd, "I_M: Atomic message");
|
||||||
|
|
||||||
add_event (SEND, NULL);
|
rd = NULL;
|
||||||
I_M = add_role ("I_M: Atomic message");
|
rd = add_event (rd, RECV, NULL);
|
||||||
|
rd = add_event (rd, RECV, NULL);
|
||||||
|
rd = add_event (rd, SEND, NULL);
|
||||||
|
I_RRS = add_role (rd, "I_E: Encrypt");
|
||||||
|
|
||||||
add_event (RECV, NULL);
|
rd = NULL;
|
||||||
add_event (RECV, NULL);
|
rd = add_event (rd, RECV, NULL);
|
||||||
add_event (SEND, NULL);
|
rd = add_event (rd, RECV, NULL);
|
||||||
I_RRS = add_role ("I_E: Encrypt");
|
rd = add_event (rd, SEND, NULL);
|
||||||
|
I_RRSD = add_role (rd, "I_D: Decrypt");
|
||||||
add_event (RECV, NULL);
|
|
||||||
add_event (RECV, NULL);
|
|
||||||
add_event (SEND, NULL);
|
|
||||||
I_RRSD = add_role ("I_D: Decrypt");
|
|
||||||
|
|
||||||
sys->num_regular_runs = 0;
|
sys->num_regular_runs = 0;
|
||||||
sys->num_intruder_runs = 0;
|
sys->num_intruder_runs = 0;
|
||||||
@ -178,31 +180,33 @@ arachneDone ()
|
|||||||
//! is this roledef already bound?
|
//! is this roledef already bound?
|
||||||
#define isBound(rd) (rd->bound)
|
#define isBound(rd) (rd->bound)
|
||||||
|
|
||||||
//! Indent prefix print
|
//! print current counter
|
||||||
void
|
void
|
||||||
indentPrefixPrint (const int annotate, const int jumps)
|
counterPrint (const int annotate)
|
||||||
{
|
{
|
||||||
void counterPrint ()
|
|
||||||
{
|
|
||||||
statesFormat (sys->current_claim->states);
|
statesFormat (sys->current_claim->states);
|
||||||
eprintf ("\t");
|
eprintf ("\t");
|
||||||
eprintf ("%i", annotate);
|
eprintf ("%i", annotate);
|
||||||
eprintf ("\t");
|
eprintf ("\t");
|
||||||
}
|
}
|
||||||
|
|
||||||
|
//! Indent prefix print
|
||||||
|
void
|
||||||
|
indentPrefixPrint (const int annotate, const int jumps)
|
||||||
|
{
|
||||||
if (switches.output == ATTACK && globalError == 0)
|
if (switches.output == ATTACK && globalError == 0)
|
||||||
{
|
{
|
||||||
// Arachne, attack, not an error
|
// Arachne, attack, not an error
|
||||||
// We assume that means DOT output
|
// We assume that means DOT output
|
||||||
eprintf ("// ");
|
eprintf ("// ");
|
||||||
counterPrint ();
|
counterPrint (annotate);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
// If it is not to stdout, or it is not an attack...
|
// If it is not to stdout, or it is not an attack...
|
||||||
int i;
|
int i;
|
||||||
|
|
||||||
counterPrint ();
|
counterPrint (annotate);
|
||||||
for (i = 0; i < jumps; i++)
|
for (i = 0; i < jumps; i++)
|
||||||
{
|
{
|
||||||
if (i % 3 == 0)
|
if (i % 3 == 0)
|
||||||
|
Loading…
Reference in New Issue
Block a user