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

- Semistate printing now reports trace length.

Browse Source 
- Pruning was wrong, so the shortest attack wasn't always found. Now it
  is.
This commit is contained in:
ccremers 2004-08-27 18:18:16 +00:00
parent 198afa135e
commit 17ad6de97b
1 changed files with 9 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
src/arachne.c
View File

@ -673,6 +673,10 @@ printSemiState ()
indentPrint (); indentPrint ();
eprintf ("!! --=[ Semistate ]=--\n"); eprintf ("!! --=[ Semistate ]=--\n");
indentPrint ();
eprintf ("!!\n");
indentPrint ();
eprintf ("!! Trace length: %i\n", get_trace_length ());
open = 0; open = 0;
for (run = 0; run < sys->maxruns; run++) for (run = 0; run < sys->maxruns; run++)
{ {
@ -1341,13 +1345,14 @@ prune_bounds ()
} }
// Limit on exceeding any attack length // Limit on exceeding any attack length
if (sys->prune == 2 && get_trace_length() >= attack_length) if (sys->prune == 2 && get_trace_length () >= attack_length)
{ {
if (sys->output == PROOF) if (sys->output == PROOF)
{ {
indentPrint (); indentPrint ();
eprintf eprintf
("Pruned: we already know an attack of length %i.\n", attack_length); ("Pruned: we already know an attack of length %i.\n",
attack_length);
} }
return 1; return 1;
} }
@ -1459,19 +1464,11 @@ property_check ()
if (sys->output == PROOF) if (sys->output == PROOF)
{ {
indentPrint (); indentPrint ();
eprintf ("New shortest attack found with trace length %i.\n", attack_length); eprintf ("New shortest attack found with trace length %i.\n",
attack_length);
} }
} }
/**
* Prune this?
*/
if (sys->prune > 0)
{
/* default: if any attack is found, abort the procedure */
flag = 0;
}
return flag; return flag;
} }