sylv/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Improved error output with line number syntax.

Browse Source
This commit is contained in:
ccremers
2007-01-29 17:20:45 +00:00
parent 33df1ccb5b
commit 41d811a49a
6 changed files with 73 additions and 22 deletions
Download Patch File Download Diff File Expand all files Collapse all files

83
src/compiler.c
View File

@@ -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 ();

2
src/role.c
View File

@@ -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;
}

5
src/role.h
View File

@@ -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.

1
src/system.c
View File

@@ -827,6 +827,7 @@ protocolCreate (Term name)
p->rolenames = NULL;
p->locals = NULL;
p->next = NULL;
p->lineno = 0;
return p;
}

1
src/system.h
View File

@@ -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.

3
src/todo.txt
View File

@@ -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