From 41d811a49aaddf3adafbb37b15c35cbba53fba84 Mon Sep 17 00:00:00 2001 From: ccremers Date: Mon, 29 Jan 2007 17:20:45 +0000 Subject: [PATCH] - Improved error output with line number syntax. --- src/compiler.c | 83 +++++++++++++++++++++++++++++++++++++------------- src/role.c | 2 ++ src/role.h | 5 +++ src/system.c | 1 + src/system.h | 1 + src/todo.txt | 3 ++ 6 files changed, 73 insertions(+), 22 deletions(-) diff --git a/src/compiler.c b/src/compiler.c index 8d50d66..0a4768a 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -398,6 +398,29 @@ levelTacDeclaration (Tac tc, int isVar) } } +//! Get last role def +Roledef +getLastRoledef (Roledef rd) +{ + if (rd != NULL) + { + while (rd->next != NULL) + { + rd = rd->next; + } + } + return rd; +} + +//! Mark last roledef lineno +void +markLastRoledef (Roledef rd, const int lineno) +{ + rd = getLastRoledef (rd); + rd->lineno = lineno; +} + + //! Check whether a claim label already occurs int isClaimlabelUsed (const System sys, const Term label) @@ -437,7 +460,7 @@ generateFreshClaimlabel (const System sys, const Protocol protocol, //! Create a claim and add it to the claims list, and add the role event. Claimlist claimCreate (const System sys, const Protocol protocol, const Role role, - const Term claim, Term label, const Term msg) + const Term claim, Term label, const Term msg, const int lineno) { Claimlist cl; @@ -501,6 +524,7 @@ claimCreate (const System sys, const Protocol protocol, const Role role, cl->roles = NULL; cl->alwaystrue = false; cl->warnings = false; + cl->lineno = lineno; /* add the claim to the end of the current list */ cl->next = NULL; @@ -523,6 +547,7 @@ claimCreate (const System sys, const Protocol protocol, const Role role, /* add the role event */ role->roledef = roledefAdd (role->roledef, CLAIM, label, role->nameterm, claim, msg, cl); + markLastRoledef (role->roledef, lineno); /* possible special handlers for each claim */ @@ -664,6 +689,8 @@ commEvent (int event, Tac tc) /* and make that read/send event */ thisRole->roledef = roledefAdd (thisRole->roledef, event, label, fromrole, torole, msg, cl); + /* mark last one with line number */ + markLastRoledef (thisRole->roledef, tc->lineno); break; case CLAIM: @@ -690,7 +717,8 @@ commEvent (int event, Tac tc) if (!inTermlist (claim->stype, TERM_Claim)) { globalError++; - eprintf ("error: claim term is not of claim type "); + eprintf ("error: [%i] claim term is not of claim type ", + trip->next->lineno); termPrint (claim); errorTac (trip->next->lineno); globalError--; @@ -768,7 +796,9 @@ commEvent (int event, Tac tc) /* create the event */ - cl = claimCreate (sys, thisProtocol, thisRole, claim, label, msg); + cl = + claimCreate (sys, thisProtocol, thisRole, claim, label, msg, + tc->lineno); } break; } @@ -821,7 +851,7 @@ claimAddAll (const System sys, const Protocol protocol, const Role role) if (realTermLeaf (t)) { // Add a secrecy claim - claimCreate (sys, protocol, role, CLAIM_Secret, NULL, t); + claimCreate (sys, protocol, role, CLAIM_Secret, NULL, t, -1); } tl = tl->next; } @@ -831,8 +861,8 @@ claimAddAll (const System sys, const Protocol protocol, const Role role) addSecrecyList (role->declaredvars); /* full non-injective agreement and ni-synch */ - claimCreate (sys, protocol, role, CLAIM_Niagree, NULL, NULL); - claimCreate (sys, protocol, role, CLAIM_Nisynch, NULL, NULL); + claimCreate (sys, protocol, role, CLAIM_Niagree, NULL, NULL, -1); + claimCreate (sys, protocol, role, CLAIM_Nisynch, NULL, NULL, -1); } //! Compile a role @@ -854,7 +884,7 @@ roleCompile (Term nameterm, Tac tc) if (thisRole == NULL) { globalError++; - eprintf ("error: undeclared role name "); + eprintf ("error: [%i] undeclared role name ", tc->lineno); termPrint (nameterm); eprintf (" in line "); errorTac (tc->lineno); @@ -900,7 +930,8 @@ roleCompile (Term nameterm, Tac tc) if (!normalDeclaration (tc)) { globalError++; - eprintf ("error: illegal command %i in role ", tc->op); + eprintf ("error: [%i] illegal command %i in role ", + tc->lineno, tc->op); termPrint (thisRole->nameterm); eprintf (" "); errorTac (tc->lineno); @@ -915,7 +946,8 @@ roleCompile (Term nameterm, Tac tc) if (switches.addreachableclaim) { - claimCreate (sys, thisProtocol, thisRole, CLAIM_Reachable, NULL, NULL); + claimCreate (sys, thisProtocol, thisRole, CLAIM_Reachable, NULL, NULL, + -1); } if (switches.addallclaims) { @@ -961,7 +993,9 @@ runInstanceCreate (Tac tc) if (p == NULL) { globalError++; - eprintf ("error: Trying to create a run of a non-declared protocol "); + eprintf + ("error: [%i] Trying to create a run of a non-declared protocol ", + tc->lineno); symbolPrint (psym); eprintf (" "); errorTac (tc->lineno); @@ -975,7 +1009,7 @@ runInstanceCreate (Tac tc) if (r == NULL) { globalError++; - eprintf ("error: Protocol "); + eprintf ("error: [%i] Protocol ", tc->lineno); symbolPrint (psym); eprintf (" has no role called "); symbolPrint (rsym); @@ -989,7 +1023,8 @@ runInstanceCreate (Tac tc) { globalError++; eprintf - ("error: Run instance has different number of parameters than protocol "); + ("error: [%i] Run instance has different number of parameters than protocol ", + tc->lineno); termPrint (p->nameterm); eprintf (" "); errorTac (tc->lineno); @@ -1055,7 +1090,8 @@ protocolCompile (Symbol prots, Tac tc, Tac tcroles) if (isTermEqual (pr->nameterm, prold->nameterm)) { globalError++; - eprintf ("error: Double declaration of protocol "); + eprintf ("error: [%i] Double declaration of protocol ", + tc->lineno); symbolPrint (prots); eprintf (" "); errorTac (tc->lineno); @@ -1127,7 +1163,8 @@ protocolCompile (Symbol prots, Tac tc, Tac tcroles) if (!normalDeclaration (tc)) { globalError++; - eprintf ("error: illegal command %i in protocol ", tc->op); + eprintf ("error: [%i] illegal command %i in protocol ", + tc->lineno, tc->op); termPrint (thisProtocol->nameterm); errorTac (tc->lineno); } @@ -1166,8 +1203,8 @@ tacProcess (Tac tc) if (!normalDeclaration (tc)) { globalError++; - eprintf ("error: illegal command %i at the global level.\n", - tc->op); + eprintf ("error: [%i] illegal command %i at the global level ", + tc->lineno, tc->op); errorTac (tc->lineno); } break; @@ -1191,7 +1228,7 @@ tacTerm (Tac tc) if (t == NULL) { globalError++; - eprintf ("error: Undeclared symbol "); + eprintf ("error: [%i] undeclared symbol ", tc->lineno); symbolPrint (tc->t1.sym); errorTac (tc->lineno); } @@ -1958,7 +1995,7 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole, if (!checkEventMatch (event, readevent)) { globalError++; - eprintf ("error:"); + eprintf ("error: [%i]", readevent->lineno); if (sys->protocols != NULL) { if (sys->protocols->next != NULL) @@ -1970,10 +2007,10 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole, eprintf (" events for label "); termPrint (event->label); eprintf (" do not match, in particular: \n"); - eprintf ("error: \t"); + eprintf ("error: [%i] ", event->lineno); roledefPrint (event); eprintf (" does not match\n"); - eprintf ("error: \t"); + eprintf ("error: [%i] ", readevent->lineno); roledefPrint (readevent); eprintf ("\n"); error_die (); @@ -2009,7 +2046,7 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole, if (found == 0) { globalError++; - eprintf ("error: for the read event "); + eprintf ("error: [%i] for the read event ", readevent->lineno); roledefPrint (readevent); eprintf (" of protocol "); termPrint (p->nameterm); @@ -2051,7 +2088,9 @@ checkLabelMatchProtocol (const System sys, const Protocol p) else { globalError++; - eprintf ("error: cannot determine label information for "); + eprintf + ("error: [%i] cannot determine label information for ", + rd->lineno); roledefPrint (rd); eprintf ("\n"); error_die (); diff --git a/src/role.c b/src/role.c index cc0c468..5b3142e 100644 --- a/src/role.c +++ b/src/role.c @@ -191,6 +191,7 @@ roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl) else newEvent->bound = 1; // other stuff does not need to be bound newEvent->next = NULL; + newEvent->lineno = 0; return newEvent; } @@ -231,6 +232,7 @@ roleCreate (Term name) r->singular = false; // by default, a role is not singular r->next = NULL; r->knows = NULL; + r->lineno = 0; return r; } diff --git a/src/role.h b/src/role.h index fa0add2..8324b43 100644 --- a/src/role.h +++ b/src/role.h @@ -54,6 +54,8 @@ struct claimlist Termlist roles; //! Next node pointer or NULL for the last element of the function. struct claimlist *next; + + int lineno; }; //! Shorthand for claimlist pointers. @@ -111,6 +113,7 @@ struct roledef /* evt runid for synchronisation, but that is implied in the base array */ + int lineno; }; //! Shorthand for roledef pointer. @@ -142,6 +145,8 @@ struct role int singular; //! Pointer to next role definition. struct role *next; + //! Line number + int lineno; }; //! Shorthand for role pointer. diff --git a/src/system.c b/src/system.c index bff3585..732e2ba 100644 --- a/src/system.c +++ b/src/system.c @@ -827,6 +827,7 @@ protocolCreate (Term name) p->rolenames = NULL; p->locals = NULL; p->next = NULL; + p->lineno = 0; return p; } diff --git a/src/system.h b/src/system.h index e982605..c65f26a 100644 --- a/src/system.h +++ b/src/system.h @@ -28,6 +28,7 @@ struct protocol Termlist locals; //! Pointer to next protocol. struct protocol *next; + int lineno; //!< Line number of definition (for errors)? }; //! Shorthand for protocol pointer. diff --git a/src/todo.txt b/src/todo.txt index 855b3f6..d3a9030 100644 --- a/src/todo.txt +++ b/src/todo.txt @@ -1,3 +1,6 @@ +- Error should have an additional line number parameter (that might be + -1 to ignore it) forcing people to use numbers :) + Format: "error: [%i] %s\n" - Nested functions should be avoided: their implementation requires an executable stack, which is bad for security purposes. However, many of the iterator functions need to pass a function and possibly some