Removed another straightforward trampoline with one nested call only.
This commit is contained in:
parent
92c5b0bedc
commit
131ee69f1d
@ -2,7 +2,6 @@
|
||||
1 subtermUnify arachne.c +961
|
||||
1 term_iterate_open_leaves dotout.c +1790 // Could be replaced by term_iterate_leaves
|
||||
3 unify mgu.c +233 ; mgu.c +247 ; mgu.c +281
|
||||
1 iterateLocalToOther prune_theorems.c +108
|
||||
|
||||
term_iterate_leaves
|
||||
term_iterate_state_leaves
|
||||
@ -13,5 +12,4 @@ iterateTermOther is called using makeDepend and addOther
|
||||
subtermUnify is called using unifiesWithKeys
|
||||
term_iterate_open_leaves is called using addsubterms
|
||||
unify is called using unify_combine_enc and unify_combined_tup, and a callback using the keys list? (which propagates back to subtermunify data)
|
||||
iterateLocalToOther is called using checkTerm
|
||||
|
||||
|
@ -41,6 +41,58 @@ extern Protocol INTRUDER;
|
||||
extern int proofDepth;
|
||||
extern int max_encryption_level;
|
||||
|
||||
//! checkTerm is a helper for the next function
|
||||
int
|
||||
checkTerm (const System sys, const Term t, const int r1)
|
||||
{
|
||||
if (!isTermVariable (t))
|
||||
{
|
||||
int r2;
|
||||
int e1, e2;
|
||||
|
||||
// t is a term from r2 that occurs in r1
|
||||
r2 = TermRunid (t);
|
||||
e1 = firstOccurrence (sys, r1, t, ANYEVENT);
|
||||
if (e1 >= 0)
|
||||
{
|
||||
if (roledef_shift (sys->runs[r1].start, e1)->type == RECV)
|
||||
{
|
||||
e2 = firstOccurrence (sys, r2, t, SEND);
|
||||
if (e2 >= 0)
|
||||
{
|
||||
// thus, it should not be the case that e1 occurs before e2
|
||||
if (isDependEvent (r1, e1, r2, e2))
|
||||
{
|
||||
// That's not good!
|
||||
if (switches.output == PROOF)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Pruned because ordering for term ");
|
||||
termSubstPrint (t);
|
||||
eprintf
|
||||
(" cannot be correct: the first send r%ii%i occurs after the receive r%ii%i.\n",
|
||||
r2, e2, r1, e1);
|
||||
}
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
globalError++;
|
||||
eprintf ("error: term ");
|
||||
termSubstPrint (t);
|
||||
eprintf
|
||||
(" from run %i should occur in run %i, but it doesn't.\n", r2,
|
||||
r1);
|
||||
globalError--;
|
||||
error ("Abort");
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
//! Check locals occurrence
|
||||
/*
|
||||
@ -51,56 +103,6 @@ correctLocalOrder (const System sys)
|
||||
{
|
||||
int r1;
|
||||
|
||||
int checkTerm (Term t)
|
||||
{
|
||||
if (!isTermVariable (t))
|
||||
{
|
||||
int r2;
|
||||
int e1, e2;
|
||||
|
||||
// t is a term from r2 that occurs in r1
|
||||
r2 = TermRunid (t);
|
||||
e1 = firstOccurrence (sys, r1, t, ANYEVENT);
|
||||
if (e1 >= 0)
|
||||
{
|
||||
if (roledef_shift (sys->runs[r1].start, e1)->type == RECV)
|
||||
{
|
||||
e2 = firstOccurrence (sys, r2, t, SEND);
|
||||
if (e2 >= 0)
|
||||
{
|
||||
// thus, it should not be the case that e1 occurs before e2
|
||||
if (isDependEvent (r1, e1, r2, e2))
|
||||
{
|
||||
// That's not good!
|
||||
if (switches.output == PROOF)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Pruned because ordering for term ");
|
||||
termSubstPrint (t);
|
||||
eprintf
|
||||
(" cannot be correct: the first send r%ii%i occurs after the receive r%ii%i.\n",
|
||||
r2, e2, r1, e1);
|
||||
}
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
globalError++;
|
||||
eprintf ("error: term ");
|
||||
termSubstPrint (t);
|
||||
eprintf
|
||||
(" from run %i should occur in run %i, but it doesn't.\n", r2,
|
||||
r1);
|
||||
globalError--;
|
||||
error ("Abort");
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
for (r1 = 0; r1 < sys->maxruns; r1++)
|
||||
{
|
||||
if (sys->runs[r1].protocol != INTRUDER)
|
||||
|
@ -1129,9 +1129,14 @@ iterateEventsType (const System sys, const int run, const int evtype,
|
||||
}
|
||||
|
||||
// Iterate over all 'others': local variables of a run that are instantiated and contain some term of another run.
|
||||
/**
|
||||
* Now incorporates "checkterm" required argument of myrun to the callback:
|
||||
*
|
||||
* It's now callback(conts Term,const int);
|
||||
*/
|
||||
int
|
||||
iterateLocalToOther (const System sys, const int myrun,
|
||||
int (*callback) (Term tlocal))
|
||||
int (*callback) (const System, const Term, const int))
|
||||
{
|
||||
Termlist tlo, tls;
|
||||
int flag;
|
||||
@ -1158,7 +1163,7 @@ iterateLocalToOther (const System sys, const int myrun,
|
||||
// now iterate over all of them
|
||||
for (tls = tlo; flag && (tls != NULL); tls = tls->next)
|
||||
{
|
||||
if (!callback (tls->term))
|
||||
if (!callback (sys, tls->term, myrun))
|
||||
{
|
||||
flag = false;
|
||||
}
|
||||
|
@ -199,7 +199,8 @@ int iterateAllEvents (const System sys,
|
||||
int iterateEventsType (const System sys, const int run, const int evtype,
|
||||
int (*callback) (Roledef rd, int ev));
|
||||
int iterateLocalToOther (const System sys, const int myrun,
|
||||
int (*callback) (Term t));
|
||||
int (*callback) (const System sys, const Term t,
|
||||
const int myrun));
|
||||
int iterateRoles (const System sys, int (*callback) (Protocol p, Role r));
|
||||
int firstOccurrence (const System sys, const int r, Term t, int evtype);
|
||||
Roledef eventRoledef (const System sys, const int run, const int ev);
|
||||
|
Loading…
Reference in New Issue
Block a user