diff --git a/src/compiler.c b/src/compiler.c index fb989b4..ed8f4e5 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -472,6 +472,16 @@ claimCreate (const System sys, const Protocol protocol, const Role role, /* then we should ignore it later */ cl->alwaystrue = true; cl->warnings = true; + + /* show a warning for this */ + globalError++; + eprintf ("warning: secrecy claim of role "); + termPrint (cl->rolename); + eprintf (" contains a variable "); + termPrint (claimvars->term); + eprintf + (" which is never read; therefore the claim will be true.\n"); + globalError--; } claimvars = claimvars->next; } @@ -1579,11 +1589,19 @@ compute_prec_sets (const System sys) //@todo This is for debugging, mainly. if (cl->prec == NULL) { - globalError++; - eprintf ("warning: claim with empty prec() set at r:%i, ev:%i\n", - r1, ev1); - globalError--; - cl->warnings = true; + if (inTermlist (CLAIMS_dep_prec, cl->type)) + { + /* this claim depends on prec, but it is empty! */ + + cl->warnings = true; + globalError++; + eprintf ("warning: claim with label "); + termPrint (cl->label); + eprintf (" of role "); + termPrint (cl->rolename); + eprintf (" has an empty prec() set.\n"); + globalError--; + } } else { diff --git a/src/specialterm.c b/src/specialterm.c index aa16b14..1607701 100644 --- a/src/specialterm.c +++ b/src/specialterm.c @@ -1,6 +1,7 @@ #include #include #include "term.h" +#include "termlist.h" #include "compiler.h" /* @@ -28,6 +29,8 @@ Term CLAIM_Niagree; Term CLAIM_Empty; Term CLAIM_Reachable; +Termlist CLAIMS_dep_prec; + //! Init special terms /** * This is called by compilerInit @@ -52,4 +55,10 @@ specialTermInit (const System sys) langcons (CLAIM_Niagree, "Niagree", TERM_Claim); langcons (CLAIM_Empty, "Empty", TERM_Claim); langcons (CLAIM_Reachable, "Reachable", TERM_Claim); + + /* Construct a list of claims that depend on prec being not-empty */ + /* basically all authentication claims */ + CLAIMS_dep_prec = termlistAdd (NULL, CLAIM_Niagree); + CLAIMS_dep_prec = termlistAdd (CLAIMS_dep_prec, CLAIM_Nisynch); + } diff --git a/src/specialterm.h b/src/specialterm.h index de0f9b3..5e877ad 100644 --- a/src/specialterm.h +++ b/src/specialterm.h @@ -1,6 +1,9 @@ #ifndef SPECIALTERM #define SPECIALTERM +#include "term.h" +#include "termlist.h" + /* * Some declarations in spercialterm.c */ @@ -20,4 +23,6 @@ extern Term CLAIM_Niagree; extern Term CLAIM_Empty; extern Term CLAIM_Reachable; +extern Termlist CLAIMS_dep_prec; + #endif