Removed dead code that nevertheless produced a trampoline warning.
This commit is contained in:
parent
15c64c8a55
commit
24c6e47f07
@ -116,110 +116,9 @@ void
|
||||
initialIntruderKnowledge (const System sys)
|
||||
{
|
||||
/*
|
||||
TODO this is buggy and leads to a segfault with Simon's example (bug report for wellformedness check)
|
||||
Disabled for now.
|
||||
./scyther-linux simple-challenge-SEGFAULT.spdl
|
||||
This was buggy and led to a segfault with Simon's example (bug report for wellformedness check);
|
||||
We didn't use it for years, but it did keep generating a trampoline for the dead code anyway. We
|
||||
therefore completely removed it during the trampoline fall cleaning of 2018.
|
||||
*/
|
||||
return;
|
||||
|
||||
/*
|
||||
* display initial role knowledge
|
||||
*/
|
||||
int deriveFromRole (Protocol p, Role r)
|
||||
{
|
||||
void addListKnowledge (Termlist tl, Term actor)
|
||||
{
|
||||
void addTermKnowledge (Term t)
|
||||
{
|
||||
if (anySubTerm (t, p->rolenames))
|
||||
{
|
||||
Term f;
|
||||
// Has rolename subterms. We have to enumerate those.
|
||||
/**
|
||||
* Hack. Enumerating is not always good (or even desirable).
|
||||
* If some I knows sk(I), sk should not be in the intruder knowledge.
|
||||
* But for hash(I), we typically would have h; but if it is never used differently, it would suffice.
|
||||
* To summarize, the operational semantics definition is perfectly fine, but maybe a bit strict sometimes.
|
||||
*
|
||||
* The hack is that if function application:
|
||||
*/
|
||||
f = getTermFunction (t);
|
||||
if (f != NULL)
|
||||
{
|
||||
// it's a function, right. So we see whether it is public. It is if it does not contain the actor...
|
||||
if (!termSubTerm (t, actor))
|
||||
{
|
||||
// no actor, then nothing secret I guess.
|
||||
addSTerm (sys, f, NULL, NULL);
|
||||
return;
|
||||
}
|
||||
else
|
||||
{
|
||||
// has actor. but does it contain even more?
|
||||
|
||||
int allagents (Term t)
|
||||
{
|
||||
if (!inTermlist (sys->agentnames, t))
|
||||
{
|
||||
if (!inTermlist (p->rolenames, t))
|
||||
{
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
if (!term_iterate_leaves (TermOp (t), allagents))
|
||||
{
|
||||
// something else as well, so that probably means a hash or something like that.
|
||||
addSTerm (sys, f, NULL, NULL);
|
||||
return;
|
||||
}
|
||||
}
|
||||
}
|
||||
// otherwise, we enumerate
|
||||
addEnumTerm (sys, t, actor, p->rolenames, NULL, NULL);
|
||||
}
|
||||
else
|
||||
{
|
||||
// No actor subterm. Simply add.
|
||||
addSTerm (sys, t, NULL, NULL);
|
||||
}
|
||||
}
|
||||
|
||||
while (tl != NULL)
|
||||
{
|
||||
addTermKnowledge (tl->term);
|
||||
tl = tl->next;
|
||||
}
|
||||
}
|
||||
|
||||
if (switches.check)
|
||||
{
|
||||
globalError++;
|
||||
eprintf ("Role ");
|
||||
termPrint (r->nameterm);
|
||||
eprintf (" knows ");
|
||||
termlistPrint (r->knows);
|
||||
eprintf ("\n");
|
||||
globalError--;
|
||||
}
|
||||
addListKnowledge (r->knows, r->nameterm);
|
||||
return true;
|
||||
}
|
||||
|
||||
if (switches.check)
|
||||
{
|
||||
globalError++;
|
||||
eprintf ("Computing initial intruder knowledge.\n\n");
|
||||
eprintf ("Agent names : ");
|
||||
termlistPrint (sys->agentnames);
|
||||
eprintf ("\n");
|
||||
eprintf ("Untrusted agents : ");
|
||||
termlistPrint (sys->untrusted);
|
||||
eprintf ("\n");
|
||||
globalError--;
|
||||
}
|
||||
|
||||
iterateRoles (sys, deriveFromRole);
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user