- Fixed the broken '--no-intruder' switch.

This commit is contained in:
ccremers 2005-12-29 12:14:21 +00:00
parent c79c9eb73f
commit a50245734d

View File

@ -2853,23 +2853,38 @@ prune_bounds ()
if (enoughAttacks (sys)) if (enoughAttacks (sys))
return 1; return 1;
// Limit on intruder events count // Pruning involving the number of intruder actions
if (switches.maxIntruderActions < INT_MAX || !(switches.intruder)) {
{ // Count intruder actions
// Only check if actually used int actioncount;
if (!(switches.intruder)
|| countIntruderActions () > switches.maxIntruderActions) actioncount = countIntruderActions ();
{
if (switches.output == PROOF) // Limit intruder actions in any case
{ if (!(switches.intruder) && actioncount > 0)
indentPrint (); {
eprintf if (switches.output == PROOF)
("Pruned: more than %i encrypt/decrypt events in the semitrace.\n", {
switches.maxIntruderActions); indentPrint ();
} eprintf
return 1; ("Pruned: no intruder allowed.\n", switches.maxIntruderActions);
} }
} return 1;
}
// Limit on intruder events count
if (actioncount > switches.maxIntruderActions)
{
if (switches.output == PROOF)
{
indentPrint ();
eprintf
("Pruned: more than %i encrypt/decrypt events in the semitrace.\n",
switches.maxIntruderActions);
}
return 1;
}
}
// No pruning because of bounds // No pruning because of bounds
return 0; return 0;