- Consistency improvements.
This commit is contained in:
parent
f219461c8d
commit
74851e0393
@ -277,7 +277,7 @@ add_intruder_goal_iterate (Goal goal)
|
|||||||
//! Bind a goal to an existing regular run, if possible
|
//! Bind a goal to an existing regular run, if possible
|
||||||
int
|
int
|
||||||
bind_existing_run (const Goal goal, const Protocol p, const Role r,
|
bind_existing_run (const Goal goal, const Protocol p, const Role r,
|
||||||
const int index)
|
const int index, const int forced_run)
|
||||||
{
|
{
|
||||||
int run, flag;
|
int run, flag;
|
||||||
|
|
||||||
@ -294,6 +294,8 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r,
|
|||||||
flag = 1;
|
flag = 1;
|
||||||
goal.rd->bind_index = index;
|
goal.rd->bind_index = index;
|
||||||
for (run = 0; run < sys->maxruns; run++)
|
for (run = 0; run < sys->maxruns; run++)
|
||||||
|
{
|
||||||
|
if (forced_run >= 0 && forced_run == run)
|
||||||
{
|
{
|
||||||
if (sys->runs[run].protocol == p && sys->runs[run].role == r)
|
if (sys->runs[run].protocol == p && sys->runs[run].role == r)
|
||||||
{
|
{
|
||||||
@ -320,6 +322,7 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r,
|
|||||||
sys->runs[run].length = old_length;
|
sys->runs[run].length = old_length;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
}
|
||||||
goal.rd->bind_run = -1;
|
goal.rd->bind_run = -1;
|
||||||
return flag;
|
return flag;
|
||||||
}
|
}
|
||||||
@ -463,7 +466,7 @@ bind_goal_regular (const Goal goal)
|
|||||||
{
|
{
|
||||||
flag = flag && bind_new_run (goal, p, r, index);
|
flag = flag && bind_new_run (goal, p, r, index);
|
||||||
}
|
}
|
||||||
return (flag && bind_existing_run (goal, p, r, index));
|
return (flag && bind_existing_run (goal, p, r, index, run));
|
||||||
}
|
}
|
||||||
|
|
||||||
if (p == INTRUDER)
|
if (p == INTRUDER)
|
||||||
@ -542,7 +545,7 @@ bind_intruder_to_regular (Goal goal)
|
|||||||
{
|
{
|
||||||
flag = flag && bind_new_run (goal, p, r, index);
|
flag = flag && bind_new_run (goal, p, r, index);
|
||||||
}
|
}
|
||||||
flag = flag && bind_existing_run (goal, p, r, index);
|
flag = flag && bind_existing_run (goal, p, r, index, run);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* deconstruct key list goals
|
* deconstruct key list goals
|
||||||
|
@ -68,7 +68,7 @@ __inline__ Term deVarScan (Term t);
|
|||||||
#define realTermLeaf(t) (t != NULL && t->type <= LEAF)
|
#define realTermLeaf(t) (t != NULL && t->type <= LEAF)
|
||||||
#define realTermTuple(t) (t != NULL && t->type == TUPLE)
|
#define realTermTuple(t) (t != NULL && t->type == TUPLE)
|
||||||
#define realTermEncrypt(t) (t != NULL && t->type == ENCRYPT)
|
#define realTermEncrypt(t) (t != NULL && t->type == ENCRYPT)
|
||||||
#define realTermVariable(t) (t != NULL && (t->type == VARIABLE || (rolelocal_variable && t->right.runid == -3)))
|
#define realTermVariable(t) (t != NULL && (t->type == VARIABLE || (t->type <= LEAF && rolelocal_variable && t->right.runid == -3)))
|
||||||
#define substVar(t) ((realTermVariable (t) && t->subst != NULL) ? 1 : 0)
|
#define substVar(t) ((realTermVariable (t) && t->subst != NULL) ? 1 : 0)
|
||||||
#define deVar(t) ( substVar(t) ? deVarScan(t->subst) : t)
|
#define deVar(t) ( substVar(t) ? deVarScan(t->subst) : t)
|
||||||
#define isTermLeaf(t) realTermLeaf(deVar(t))
|
#define isTermLeaf(t) realTermLeaf(deVar(t))
|
||||||
|
Loading…
Reference in New Issue
Block a user