From e19f8bddd16cf5ac9316728622baf1cd65d27dda Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 28 Dec 2005 14:42:46 +0000 Subject: [PATCH] - Improved Reachable claims output - Use square brackets for remark output instead of normal brackets. --- src/main.c | 30 +++++++++++++++++++++++------- 1 file changed, 23 insertions(+), 7 deletions(-) diff --git a/src/main.c b/src/main.c index 9a730dd..6538db5 100644 --- a/src/main.c +++ b/src/main.c @@ -456,9 +456,20 @@ timersPrint (const System sys) if (cl_scan->count > 0 && cl_scan->failed > 0) { /* there is an attack */ - eprintf ("yes\t"); + if (!isTermEqual (cl_scan->type, CLAIM_Reachable)) + { + /* a normal claim */ + eprintf ("yes"); + } + else + { + /* Reachable is not an attack */ + eprintf ("no"); + } + + eprintf ("\t"); /* are these all attacks? */ - eprintf ("("); + eprintf ("["); if (cl_scan->complete) { eprintf ("exactly"); @@ -467,7 +478,12 @@ timersPrint (const System sys) { eprintf ("at least"); } - eprintf (" %i)", cl_scan->failed); + eprintf (" %i variant", cl_scan->failed); + if (cl_scan->failed != 1) + { + eprintf ("s"); + } + eprintf ("]"); } else { @@ -478,7 +494,7 @@ timersPrint (const System sys) if (cl_scan->count == 0) { /* not encountered */ - eprintf ("(does not occur)"); + eprintf ("[does not occur]"); } else { @@ -486,12 +502,12 @@ timersPrint (const System sys) if (cl_scan->complete) { /* complete proof */ - eprintf ("(proof of correctness)"); + eprintf ("[proof of correctness]"); } else { /* only due to bounds */ - eprintf ("(no attack within bounds)"); + eprintf ("[no attack within bounds]"); if (cl_scan->timebound) eprintf ("\ttime=%i", get_time_limit ()); } @@ -501,7 +517,7 @@ timersPrint (const System sys) /* any warnings */ if (cl_scan->warnings) { - eprintf ("\t(read the warnings for more information)"); + eprintf ("\t[read the warnings for more information]"); } /* proceed to next claim */