From 17ad6de97b9aac6ac34686a099689a24a65b9b52 Mon Sep 17 00:00:00 2001 From: ccremers Date: Fri, 27 Aug 2004 18:18:16 +0000 Subject: [PATCH] - Semistate printing now reports trace length. - Pruning was wrong, so the shortest attack wasn't always found. Now it is. --- src/arachne.c | 21 +++++++++------------ 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index be4ea60..3fa8c62 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -673,6 +673,10 @@ printSemiState () indentPrint (); eprintf ("!! --=[ Semistate ]=--\n"); + indentPrint (); + eprintf ("!!\n"); + indentPrint (); + eprintf ("!! Trace length: %i\n", get_trace_length ()); open = 0; for (run = 0; run < sys->maxruns; run++) { @@ -1341,13 +1345,14 @@ prune_bounds () } // 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) { indentPrint (); 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; } @@ -1459,19 +1464,11 @@ property_check () if (sys->output == PROOF) { 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; }