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

Removed another simple trampoline.

Browse Source
This commit is contained in:
Cas Cremers 2018-10-21 18:52:20 +02:00
parent d9e17005ae
commit 1c81b04aa2
1 changed files with 58 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

115
src/prune_theorems.c
View File

@ -49,68 +49,69 @@ extern int max_encryption_level;
int int
correctLocalOrder (const System sys) correctLocalOrder (const System sys)
{ {
int flag; int r1;
int checkRun (int r1) int checkTerm (Term t)
{ {
int checkTerm (Term t) if (!isTermVariable (t))
{ {
if (!isTermVariable (t)) int r2;
{ int e1, e2;
int r2;
int e1, e2;
// t is a term from r2 that occurs in r1 // t is a term from r2 that occurs in r1
r2 = TermRunid (t); r2 = TermRunid (t);
e1 = firstOccurrence (sys, r1, t, ANYEVENT); e1 = firstOccurrence (sys, r1, t, ANYEVENT);
if (e1 >= 0) if (e1 >= 0)
{ {
if (roledef_shift (sys->runs[r1].start, e1)->type == RECV) if (roledef_shift (sys->runs[r1].start, e1)->type == RECV)
{ {
e2 = firstOccurrence (sys, r2, t, SEND); e2 = firstOccurrence (sys, r2, t, SEND);
if (e2 >= 0) if (e2 >= 0)
{ {
// thus, it should not be the case that e1 occurs before e2 // thus, it should not be the case that e1 occurs before e2
if (isDependEvent (r1, e1, r2, e2)) if (isDependEvent (r1, e1, r2, e2))
{ {
// That's not good! // That's not good!
if (switches.output == PROOF) if (switches.output == PROOF)
{ {
indentPrint (); indentPrint ();
eprintf ("Pruned because ordering for term "); eprintf ("Pruned because ordering for term ");
termSubstPrint (t); termSubstPrint (t);
eprintf eprintf
(" cannot be correct: the first send r%ii%i occurs after the receive r%ii%i.\n", (" cannot be correct: the first send r%ii%i occurs after the receive r%ii%i.\n",
r2, e2, r1, e1); r2, e2, r1, e1);
} }
flag = false; return false;
return false; }
} }
} }
} }
} else
else {
{ globalError++;
globalError++; eprintf ("error: term ");
eprintf ("error: term "); termSubstPrint (t);
termSubstPrint (t); eprintf
eprintf (" from run %i should occur in run %i, but it doesn't.\n", r2,
(" from run %i should occur in run %i, but it doesn't.\n", r2, r1);
r1); globalError--;
globalError--; error ("Abort");
error ("Abort"); }
} }
} return true;
return true;
}
return iterateLocalToOther (sys, r1, checkTerm);
} }
flag = true; for (r1 = 0; r1 < sys->maxruns; r1++)
iterateRegularRuns (sys, checkRun); {
if (sys->runs[r1].protocol != INTRUDER)
return flag; {
if (!iterateLocalToOther (sys, r1, checkTerm))
{
return false;
}
}
}
return true;
} }
//! Check all runs //! Check all runs