andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Minor refactoring.

Browse Source
This commit is contained in:
ccremers 2006-08-08 14:50:28 +00:00
parent d2e3aaa869
commit 341bbfeb0c
1 changed files with 123 additions and 117 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

240
src/arachne.c
View File

@ -2231,7 +2231,128 @@ iterate_buffer_attacks (void)
}
}
//! Arachne single claim
//! Arachne single claim test
int
arachneClaimTest (Claimlist cl)
{
// others we simply test...
int run;
int newruns;
Protocol p;
Role r;
newruns = 0;
sys->current_claim = cl;
attack_length = INT_MAX;
attack_leastcost = INT_MAX;
cl->complete = 1;
p = (Protocol) cl->protocol;
r = (Role) cl->role;
if (switches.output == PROOF)
{
indentPrint ();
eprintf ("Testing Claim ");
termPrint (cl->type);
eprintf (" from ");
termPrint (p->nameterm);
eprintf (", ");
termPrint (r->nameterm);
eprintf (" at index %i.\n", cl->ev);
}
indentDepth++;
run = semiRunCreate (p, r);
newruns++;
{
int newgoals;
int realStart (void)
{
#ifdef DEBUG
if (DEBUGL (5))
{
printSemiState ();
}
#endif
return iterate_buffer_attacks ();
}
proof_suppose_run (run, 0, cl->ev + 1);
newgoals = add_read_goals (run, 0, cl->ev + 1);
/**
* Add initial knowledge node
*/
{
Termlist m0tl;
Term m0t;
int m0run;
m0tl = knowledgeSet (sys->know);
m0t = termlist_to_tuple (m0tl);
// eprintf("Initial intruder knowledge node for ");
// termPrint(m0t);
// eprintf("\n");
I_M->roledef->message = m0t;
m0run = semiRunCreate (INTRUDER, I_M);
newruns++;
proof_suppose_run (m0run, 0, 1);
sys->runs[m0run].height = 1;
{
/**
* Add specific goal info and iterate algorithm
*/
add_claim_specifics (sys, cl,
roledef_shift (sys->runs[run].
start, cl->ev), realStart);
}
// remove initial knowledge node
termDelete (m0t);
termlistDelete (m0tl);
semiRunDestroy ();
newruns--;
}
// remove claiming run goals
goal_remove_last (newgoals);
semiRunDestroy ();
newruns--;
}
//! Destroy
while (sys->maxruns > 0 && newruns > 0)
{
semiRunDestroy ();
newruns--;
}
#ifdef DEBUG
if (sys->bindings != NULL)
{
error ("sys->bindings NOT empty after claim test.");
}
if (sys->maxruns != 0)
{
error ("%i undestroyed runs left after claim test.", sys->maxruns);
}
if (newruns != 0)
{
error ("Lost %i runs after claim test.", newruns);
}
#endif
//! Indent back
indentDepth--;
if (switches.output == PROOF)
{
indentPrint ();
eprintf ("Proof complete for this claim.\n");
}
}
//! Arachne single claim inspection
int
arachneClaim (Claimlist cl)
{
@ -2242,122 +2363,7 @@ arachneClaim (Claimlist cl)
if (!cl->alwaystrue)
{
// others we simply test...
int run;
int newruns;
Protocol p;
Role r;
newruns = 0;
sys->current_claim = cl;
attack_length = INT_MAX;
attack_leastcost = INT_MAX;
cl->complete = 1;
p = (Protocol) cl->protocol;
r = (Role) cl->role;
if (switches.output == PROOF)
{
indentPrint ();
eprintf ("Testing Claim ");
termPrint (cl->type);
eprintf (" from ");
termPrint (p->nameterm);
eprintf (", ");
termPrint (r->nameterm);
eprintf (" at index %i.\n", cl->ev);
}
indentDepth++;
run = semiRunCreate (p, r);
newruns++;
{
int newgoals;
int realStart (void)
{
#ifdef DEBUG
if (DEBUGL (5))
{
printSemiState ();
}
#endif
return iterate_buffer_attacks ();
}
proof_suppose_run (run, 0, cl->ev + 1);
newgoals = add_read_goals (run, 0, cl->ev + 1);
/**
* Add initial knowledge node
*/
{
Termlist m0tl;
Term m0t;
int m0run;
m0tl = knowledgeSet (sys->know);
m0t = termlist_to_tuple (m0tl);
// eprintf("Initial intruder knowledge node for ");
// termPrint(m0t);
// eprintf("\n");
I_M->roledef->message = m0t;
m0run = semiRunCreate (INTRUDER, I_M);
newruns++;
proof_suppose_run (m0run, 0, 1);
sys->runs[m0run].height = 1;
{
/**
* Add specific goal info and iterate algorithm
*/
add_claim_specifics (sys, cl,
roledef_shift (sys->runs[run].
start, cl->ev),
realStart);
}
// remove initial knowledge node
termDelete (m0t);
termlistDelete (m0tl);
semiRunDestroy ();
newruns--;
}
// remove claiming run goals
goal_remove_last (newgoals);
semiRunDestroy ();
newruns--;
}
//! Destroy
while (sys->maxruns > 0 && newruns > 0)
{
semiRunDestroy ();
newruns--;
}
#ifdef DEBUG
if (sys->bindings != NULL)
{
error ("sys->bindings NOT empty after claim test.");
}
if (sys->maxruns != 0)
{
error ("%i undestroyed runs left after claim test.",
sys->maxruns);
}
if (newruns != 0)
{
error ("Lost %i runs after claim test.", newruns);
}
#endif
//! Indent back
indentDepth--;
if (switches.output == PROOF)
{
indentPrint ();
eprintf ("Proof complete for this claim.\n");
}
arachneClaimTest (cl);
}
claimStatusReport (sys, cl);
if (switches.xml)