- Some added error/bounds detection all around.
This commit is contained in:
parent
a673ea4ad1
commit
0e9b7dcf11
@ -175,7 +175,7 @@ int
|
||||
isTermFunctionName (Term t)
|
||||
{
|
||||
t = deVar (t);
|
||||
if (t != NULL && isTermLeaf(t) && inTermlist (t->stype, TERM_Function))
|
||||
if (t != NULL && isTermLeaf(t) && t->stype != NULL && inTermlist (t->stype, TERM_Function))
|
||||
return 1;
|
||||
return 0;
|
||||
}
|
||||
@ -1470,6 +1470,10 @@ prune_theorems ()
|
||||
Term agent;
|
||||
|
||||
agent = deVar (tl->term);
|
||||
if (agent == NULL)
|
||||
{
|
||||
error ("Agent of run 0 is NULL");
|
||||
}
|
||||
if (!realTermLeaf (agent))
|
||||
{
|
||||
if (sys->output == PROOF)
|
||||
@ -1511,16 +1515,38 @@ prune_theorems ()
|
||||
{
|
||||
if (sys->runs[run].protocol != INTRUDER)
|
||||
{
|
||||
Term actor;
|
||||
|
||||
actor = agentOfRun(sys, run);
|
||||
if (inTermlist (sys->untrusted, actor))
|
||||
if (sys->runs[run].agents != NULL)
|
||||
{
|
||||
if (sys->output == PROOF)
|
||||
Term actor;
|
||||
|
||||
actor = agentOfRun(sys, run);
|
||||
if (actor == NULL)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Pruned because the actor of run %i is untrusted.\n", run);
|
||||
error ("Agent of run %i is NULL", run);
|
||||
}
|
||||
if (inTermlist (sys->untrusted, actor))
|
||||
{
|
||||
if (sys->output == PROOF)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Pruned because the actor of run %i is untrusted.\n", run);
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
Protocol p;
|
||||
|
||||
globalError++;
|
||||
eprintf ("Run %i: ", run);
|
||||
role_name_print (run);
|
||||
eprintf (" has an empty agents list.\n");
|
||||
eprintf ("protocol->rolenames: ");
|
||||
p = (Protocol) sys->runs[run].protocol;
|
||||
termlistPrint (p->rolenames);
|
||||
eprintf ("\n");
|
||||
error ("Aborting.");
|
||||
globalError--;
|
||||
}
|
||||
}
|
||||
run++;
|
||||
|
@ -513,6 +513,10 @@ commEvent (int event, Tac tc)
|
||||
|
||||
/* store claim in claim list */
|
||||
|
||||
if (label == NULL)
|
||||
{
|
||||
error ("Claim should have label on line %i.", trip->next->lineno);
|
||||
}
|
||||
// First check whether label is unique
|
||||
cl = sys->claimlist;
|
||||
while (cl != NULL)
|
||||
|
@ -232,6 +232,12 @@ symbol_fix_keylevels (void)
|
||||
if (sym->keylevel == INT_MAX)
|
||||
{
|
||||
// Nothing currently, this simply does not originate on a strand.
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
eprintf (" doesn't have a keylevel yet.\n");
|
||||
}
|
||||
#endif
|
||||
}
|
||||
#ifdef DEBUG
|
||||
else
|
||||
|
@ -508,7 +508,6 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
|
||||
Termlist tolist = NULL;
|
||||
Termlist artefacts = NULL;
|
||||
Term extterm = NULL;
|
||||
Term newvar;
|
||||
|
||||
/* claim runid, allocate space */
|
||||
rid = sys->maxruns;
|
||||
@ -538,6 +537,8 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
|
||||
if (scanto->term->stype != NULL &&
|
||||
inTermlist (scanto->term->stype, TERM_Type))
|
||||
{
|
||||
Term newvar;
|
||||
|
||||
/* There is a TYPE constant in the parameter list.
|
||||
* Generate a new local variable for this run, with this type */
|
||||
newvar =
|
||||
|
Loading…
Reference in New Issue
Block a user