From ff87bf180fa9773d70e2b8daaf974185c42d06c6 Mon Sep 17 00:00:00 2001 From: ccremers Date: Tue, 1 Aug 2006 05:58:02 +0000 Subject: [PATCH] - Claim reporting moved into claim.c --- src/claim.c | 185 ++++++++++++++++++++++++++++++++++++++++++++++++++++ src/claim.h | 1 + src/main.c | 175 +------------------------------------------------ 3 files changed, 188 insertions(+), 173 deletions(-) diff --git a/src/claim.c b/src/claim.c index fcbb333..dd36d3c 100644 --- a/src/claim.c +++ b/src/claim.c @@ -847,3 +847,188 @@ property_check (const System sys) return flag; } + +//! Report claim status +int +claimStatusReport (const System sys, Claimlist cl) +{ + if (isTermEqual (cl->type, CLAIM_Empty)) + { + return false; + } + else + { + Protocol protocol; + Term pname; + Term rname; + Termlist labellist; + int isAttack; // stores whether this claim failure constitutes an attack or not + + if (switches.output != SUMMARY) + { + globalError++; + } + if (isTermEqual (cl->type, CLAIM_Reachable)) + { + // An attack on reachable is not really an attack, we're just generating the state space + isAttack = false; + } + else + { + isAttack = true; + } + + eprintf ("claim\t"); + + protocol = (Protocol) cl->protocol; + pname = protocol->nameterm; + rname = cl->rolename; + + labellist = tuple_to_termlist (cl->label); + + /* maybe the label contains duplicate info: if so, we remove it here */ + { + Termlist tl; + tl = labellist; + while (tl != NULL) + { + if (isTermEqual (tl->term, pname) + || isTermEqual (tl->term, rname)) + { + tl = termlistDelTerm (tl); + labellist = tl; + } + else + { + tl = tl->next; + } + } + } + + termPrint (pname); + eprintf (","); + termPrint (rname); + eprintf ("\t"); + /* second print event_label */ + termPrint (cl->type); + + eprintf ("_"); + if (labellist != NULL) + { + Termlist tl; + + tl = labellist; + while (tl != NULL) + { + termPrint (tl->term); + tl = tl->next; + if (tl != NULL) + { + eprintf (","); + } + } + /* clean up */ + termlistDelete (labellist); + labellist = NULL; + } + else + { + eprintf ("?"); + } + /* add parameter */ + eprintf ("\t"); + if (cl->parameter != NULL) + { + termPrint (cl->parameter); + } + else + { + eprintf ("-"); + } + + /* now report the status */ + eprintf ("\t"); + if (cl->count > 0 && cl->failed > 0) + { + /* there is a state */ + printOkFail (true, isAttack); + + eprintf ("\t"); + /* are these all attacks? */ + eprintf ("["); + if (cl->complete) + { + eprintf ("exactly"); + } + else + { + eprintf ("at least"); + } + eprintf (" %i ", cl->failed); + if (isAttack) + { + eprintf ("attack"); + } + else + { + eprintf ("variant"); + } + if (cl->failed != 1) + { + eprintf ("s"); + } + eprintf ("]"); + } + else + { + /* no state */ + printOkFail (false, isAttack); + eprintf ("\t"); + + /* subcases */ + if (cl->count == 0) + { + /* not encountered */ + eprintf ("[does not occur]"); + } + else + { + /* does occur */ + if (cl->complete) + { + /* complete proof */ + eprintf ("[proof of correctness]"); + } + else + { + /* only due to bounds */ + eprintf ("[no attack within bounds]"); + } + } + if (cl->timebound) + eprintf ("\ttime=%i", get_time_limit ()); + } + + /* states (if asked) */ + if (switches.countStates) + { + eprintf ("\tstates="); + statesFormat (cl->states); + } + + /* any warnings */ + if (cl->warnings) + { + eprintf ("\t[read the warnings for more information]"); + } + + /* new line */ + eprintf ("\n"); + + if (switches.output != SUMMARY) + { + globalError--; + } + return true; + } +} diff --git a/src/claim.h b/src/claim.h index d15798e..bf916c8 100644 --- a/src/claim.h +++ b/src/claim.h @@ -13,5 +13,6 @@ int add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd, int (*callback) (void)); void count_false_claim (const System sys); int property_check (const System sys); +int claimStatusReport (const System sys, Claimlist cl); #endif diff --git a/src/main.c b/src/main.c index d7f2725..2533d55 100644 --- a/src/main.c +++ b/src/main.c @@ -53,6 +53,7 @@ #include "specialterm.h" #include "color.h" #include "error.h" +#include "claim.h" //! The global system state pointer System sys; @@ -266,10 +267,6 @@ timersPrint (const System sys) // #define NOTIMERS /* display stats */ - if (switches.output != SUMMARY) - { - globalError++; - } //********************************************************************** @@ -280,171 +277,9 @@ timersPrint (const System sys) anyclaims = false; while (cl_scan != NULL) { - if (!isTermEqual (cl_scan->type, CLAIM_Empty)) + if (claimStatusReport (sys, cl_scan)) { - Protocol protocol; - Term pname; - Term rname; - Termlist labellist; - int isAttack; // stores whether this claim failure constitutes an attack or not - - if (isTermEqual (cl_scan->type, CLAIM_Reachable)) - { - // An attack on reachable is not really an attack, we're just generating the state space - isAttack = false; - } - else - { - isAttack = true; - } anyclaims = true; - - eprintf ("claim\t"); - - protocol = (Protocol) cl_scan->protocol; - pname = protocol->nameterm; - rname = cl_scan->rolename; - - labellist = tuple_to_termlist (cl_scan->label); - - /* maybe the label contains duplicate info: if so, we remove it here */ - { - Termlist tl; - tl = labellist; - while (tl != NULL) - { - if (isTermEqual (tl->term, pname) - || isTermEqual (tl->term, rname)) - { - tl = termlistDelTerm (tl); - labellist = tl; - } - else - { - tl = tl->next; - } - } - } - - termPrint (pname); - eprintf (","); - termPrint (rname); - eprintf ("\t"); - /* second print event_label */ - termPrint (cl_scan->type); - - eprintf ("_"); - if (labellist != NULL) - { - Termlist tl; - - tl = labellist; - while (tl != NULL) - { - termPrint (tl->term); - tl = tl->next; - if (tl != NULL) - { - eprintf (","); - } - } - /* clean up */ - termlistDelete (labellist); - labellist = NULL; - } - else - { - eprintf ("?"); - } - /* add parameter */ - eprintf ("\t"); - if (cl_scan->parameter != NULL) - { - termPrint (cl_scan->parameter); - } - else - { - eprintf ("-"); - } - - /* now report the status */ - eprintf ("\t"); - if (cl_scan->count > 0 && cl_scan->failed > 0) - { - /* there is a state */ - printOkFail (true, isAttack); - - eprintf ("\t"); - /* are these all attacks? */ - eprintf ("["); - if (cl_scan->complete) - { - eprintf ("exactly"); - } - else - { - eprintf ("at least"); - } - eprintf (" %i ", cl_scan->failed); - if (isAttack) - { - eprintf ("attack"); - } - else - { - eprintf ("variant"); - } - if (cl_scan->failed != 1) - { - eprintf ("s"); - } - eprintf ("]"); - } - else - { - /* no state */ - printOkFail (false, isAttack); - eprintf ("\t"); - - /* subcases */ - if (cl_scan->count == 0) - { - /* not encountered */ - eprintf ("[does not occur]"); - } - else - { - /* does occur */ - if (cl_scan->complete) - { - /* complete proof */ - eprintf ("[proof of correctness]"); - } - else - { - /* only due to bounds */ - eprintf ("[no attack within bounds]"); - } - } - if (cl_scan->timebound) - eprintf ("\ttime=%i", get_time_limit ()); - } - - /* states (if asked) */ - if (switches.countStates) - { - eprintf ("\tstates="); - statesFormat (cl_scan->states); - } - - /* any warnings */ - if (cl_scan->warnings) - { - eprintf ("\t[read the warnings for more information]"); - } - - /* proceed to next claim */ - eprintf ("\n"); } cl_scan = cl_scan->next; } @@ -452,12 +287,6 @@ timersPrint (const System sys) { warning ("No claims in system."); } - - /* reset globalError */ - if (switches.output != SUMMARY) - { - globalError--; - } } //! Analyse the model