- Some minor cleanups.
This commit is contained in:
parent
4832e9116c
commit
b04bc86185
@ -175,7 +175,7 @@ int
|
|||||||
isTermFunctionName (Term t)
|
isTermFunctionName (Term t)
|
||||||
{
|
{
|
||||||
t = deVar (t);
|
t = deVar (t);
|
||||||
if (t != NULL && inTermlist (t->stype, TERM_Function))
|
if (t != NULL && isTermLeaf(t) && inTermlist (t->stype, TERM_Function))
|
||||||
return 1;
|
return 1;
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
@ -1259,17 +1259,16 @@ bind_goal_regular_run (const Binding b)
|
|||||||
int flag;
|
int flag;
|
||||||
int found;
|
int found;
|
||||||
|
|
||||||
|
int test_sub_unification (Termlist substlist, Termlist keylist)
|
||||||
|
{
|
||||||
|
// A unification exists; return the signal
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
/*
|
/*
|
||||||
* This is a local function so we have access to goal
|
* This is a local function so we have access to goal
|
||||||
*/
|
*/
|
||||||
int bind_this_role_send (Protocol p, Role r, Roledef rd, int index)
|
int bind_this_role_send (Protocol p, Role r, Roledef rd, int index)
|
||||||
{
|
{
|
||||||
int test_unification (Termlist substlist)
|
|
||||||
{
|
|
||||||
// A unification exists; return the signal
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
if (p == INTRUDER)
|
if (p == INTRUDER)
|
||||||
{
|
{
|
||||||
// No intruder roles here
|
// No intruder roles here
|
||||||
@ -1291,7 +1290,7 @@ bind_goal_regular_run (const Binding b)
|
|||||||
}
|
}
|
||||||
#endif
|
#endif
|
||||||
if (!termMguSubTerm
|
if (!termMguSubTerm
|
||||||
(b->term, rd->message, test_unification, sys->know->inverses, NULL))
|
(b->term, rd->message, test_sub_unification, sys->know->inverses, NULL))
|
||||||
{
|
{
|
||||||
int flag;
|
int flag;
|
||||||
|
|
||||||
|
14
src/mgu.c
14
src/mgu.c
@ -239,7 +239,7 @@ termMguTerm (Term t1, Term t2)
|
|||||||
*@returns Nothing. Iteration gets termlist of substitutions.
|
*@returns Nothing. Iteration gets termlist of substitutions.
|
||||||
*/
|
*/
|
||||||
int
|
int
|
||||||
termMguInTerm (Term t1, Term t2, int (*iterator) ())
|
termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist))
|
||||||
{
|
{
|
||||||
Termlist tl;
|
Termlist tl;
|
||||||
int flag;
|
int flag;
|
||||||
@ -282,16 +282,18 @@ termMguInTerm (Term t1, Term t2, int (*iterator) ())
|
|||||||
*@returns Nothing. Iteration gets termlist of subst, and list of keys needed to decrypt.
|
*@returns Nothing. Iteration gets termlist of subst, and list of keys needed to decrypt.
|
||||||
*/
|
*/
|
||||||
int
|
int
|
||||||
termMguSubTerm (Term t1, Term t2, int (*iterator) (),
|
termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
|
||||||
Termlist inverses, Termlist keylist)
|
Termlist inverses, Termlist keylist)
|
||||||
{
|
{
|
||||||
int flag;
|
int flag;
|
||||||
Termlist tl;
|
|
||||||
|
|
||||||
flag = 1;
|
flag = 1;
|
||||||
|
t1 = deVar (t1);
|
||||||
t2 = deVar (t2);
|
t2 = deVar (t2);
|
||||||
if (t2 != NULL)
|
if (t2 != NULL)
|
||||||
{
|
{
|
||||||
|
Termlist tl;
|
||||||
|
|
||||||
if (!realTermLeaf (t2))
|
if (!realTermLeaf (t2))
|
||||||
{
|
{
|
||||||
if (realTermTuple (t2))
|
if (realTermTuple (t2))
|
||||||
@ -308,14 +310,14 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (),
|
|||||||
{
|
{
|
||||||
// Must be encryption
|
// Must be encryption
|
||||||
// So, we need the key, and try to get the rest
|
// So, we need the key, and try to get the rest
|
||||||
Termlist keylist_new;
|
|
||||||
Term newkey;
|
Term newkey;
|
||||||
|
|
||||||
newkey = inverseKey (inverses, t2->right.key);
|
newkey = inverseKey (inverses, t2->right.key);
|
||||||
|
|
||||||
// We can never produce the TERM_Hidden key, thus, this is not a valid iteration.
|
// We can never produce the TERM_Hidden key, thus, this is not a valid iteration.
|
||||||
if (!isTermEqual (newkey, TERM_Hidden))
|
if (!isTermEqual (newkey, TERM_Hidden))
|
||||||
{
|
{
|
||||||
|
Termlist keylist_new;
|
||||||
|
|
||||||
keylist_new = termlistShallow (keylist);
|
keylist_new = termlistShallow (keylist);
|
||||||
keylist_new = termlistAdd (keylist_new, newkey);
|
keylist_new = termlistAdd (keylist_new, newkey);
|
||||||
|
|
||||||
@ -343,7 +345,7 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (),
|
|||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
if (deVar (t1) != NULL)
|
if (t1 != NULL)
|
||||||
{
|
{
|
||||||
flag = 0;
|
flag = 0;
|
||||||
}
|
}
|
||||||
|
@ -15,8 +15,8 @@
|
|||||||
#define MGUFAIL (Termlist) -1
|
#define MGUFAIL (Termlist) -1
|
||||||
|
|
||||||
Termlist termMguTerm (Term t1, Term t2);
|
Termlist termMguTerm (Term t1, Term t2);
|
||||||
int termMguInTerm (Term t1, Term t2, int (*iterator) ());
|
int termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist));
|
||||||
int termMguSubTerm (Term t1, Term t2, int (*iterator) (),
|
int termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
|
||||||
Termlist inverses, Termlist keylist);
|
Termlist inverses, Termlist keylist);
|
||||||
void termlistSubstReset (Termlist tl);
|
void termlistSubstReset (Termlist tl);
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user