diff --git a/src/arachne.c b/src/arachne.c index f72a88e..473cb2c 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -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++; diff --git a/src/compiler.c b/src/compiler.c index 25008ab..f3996d4 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -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) diff --git a/src/symbol.c b/src/symbol.c index 18c375f..42a4b59 100644 --- a/src/symbol.c +++ b/src/symbol.c @@ -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 diff --git a/src/system.c b/src/system.c index 78e8ca7..98f6d85 100644 --- a/src/system.c +++ b/src/system.c @@ -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 =