- Fixed a bug in mgu.c (& instead of &&)
- scons shared=yes is now okay for Valgrind.
This commit is contained in:
parent
758cb88c8c
commit
54d857ca3c
@ -110,17 +110,19 @@ arachneDone ()
|
|||||||
#define isBound(rd) (rd->bind_run != INVALID)
|
#define isBound(rd) (rd->bind_run != INVALID)
|
||||||
#define length step
|
#define length step
|
||||||
|
|
||||||
#ifdef DEBUG
|
|
||||||
//! Indent print
|
//! Indent print
|
||||||
void
|
void
|
||||||
indentPrint ()
|
indentPrint ()
|
||||||
{
|
{
|
||||||
|
#ifdef DEBUG
|
||||||
int i;
|
int i;
|
||||||
|
|
||||||
for (i = 0; i < indentDepth; i++)
|
for (i = 0; i < indentDepth; i++)
|
||||||
eprintf ("| ");
|
eprintf ("| ");
|
||||||
}
|
#else
|
||||||
|
eprintf (">> ");
|
||||||
#endif
|
#endif
|
||||||
|
}
|
||||||
|
|
||||||
//! Iterate but discard the info of the termlist
|
//! Iterate but discard the info of the termlist
|
||||||
int
|
int
|
||||||
@ -384,15 +386,14 @@ bind_goal_regular (const Goal goal)
|
|||||||
}
|
}
|
||||||
|
|
||||||
// Bind to all possible sends or intruder node;
|
// Bind to all possible sends or intruder node;
|
||||||
return (iterate_role_sends (bind_this) &&
|
return (iterate_role_sends (bind_this) && add_intruder_goal_iterate (goal));
|
||||||
add_intruder_goal_iterate (goal));
|
|
||||||
}
|
}
|
||||||
|
|
||||||
//! Bind an intruder goal to a regular run
|
//! Bind an intruder goal to a regular run
|
||||||
int
|
int
|
||||||
bind_intruder_to_regular (const Goal goal)
|
bind_intruder_to_regular (const Goal goal)
|
||||||
{
|
{
|
||||||
int bind_this (Protocol p, Role r, Roledef rd, int index)
|
int bind_this_f2 (Protocol p, Role r, Roledef rd, int index)
|
||||||
{
|
{
|
||||||
int element_f2 (Termlist substlist, Termlist keylist)
|
int element_f2 (Termlist substlist, Termlist keylist)
|
||||||
{
|
{
|
||||||
@ -413,12 +414,12 @@ bind_intruder_to_regular (const Goal goal)
|
|||||||
* In any case, the list of keys is added as a new goal.
|
* In any case, the list of keys is added as a new goal.
|
||||||
*/
|
*/
|
||||||
int add_key_goal (Term t)
|
int add_key_goal (Term t)
|
||||||
{
|
{
|
||||||
keygoals++;
|
keygoals++;
|
||||||
create_intruder_goal (t);
|
create_intruder_goal (t);
|
||||||
//!@todo This needs a mapping Pi relation as well.
|
//!@todo This needs a mapping Pi relation as well.
|
||||||
return 1;
|
return 1;
|
||||||
}
|
}
|
||||||
|
|
||||||
keygoals = 0;
|
keygoals = 0;
|
||||||
termlist_iterate (keylist, add_key_goal);
|
termlist_iterate (keylist, add_key_goal);
|
||||||
@ -427,8 +428,13 @@ bind_intruder_to_regular (const Goal goal)
|
|||||||
* or from a new one.
|
* or from a new one.
|
||||||
*/
|
*/
|
||||||
|
|
||||||
flag = bind_existing_run (goal, p, r, index) &&
|
/**
|
||||||
bind_new_run (goal, p, r, index);
|
* This code has a major bug (memory destruction)
|
||||||
|
* in both branches
|
||||||
|
*@todo FIX!!
|
||||||
|
*/
|
||||||
|
flag = bind_existing_run (goal, p, r, index)
|
||||||
|
&& bind_new_run (goal, p, r, index);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* deconstruct key list goals
|
* deconstruct key list goals
|
||||||
@ -444,11 +450,12 @@ bind_intruder_to_regular (const Goal goal)
|
|||||||
}
|
}
|
||||||
|
|
||||||
// Test for subterm unification
|
// Test for subterm unification
|
||||||
return termMguSubTerm (goal.rd->message, rd->message, element_f2, sys->traceKnow[0]->inverses, NULL);
|
return termMguSubTerm (goal.rd->message, rd->message, element_f2,
|
||||||
|
sys->traceKnow[0]->inverses, NULL);
|
||||||
}
|
}
|
||||||
|
|
||||||
// Bind to all possible sends?
|
// Bind to all possible sends?
|
||||||
return iterate_role_sends (bind_this);
|
return iterate_role_sends (bind_this_f2);
|
||||||
}
|
}
|
||||||
|
|
||||||
//! Bind an intruder goal by intruder construction
|
//! Bind an intruder goal by intruder construction
|
||||||
|
@ -198,7 +198,7 @@ termMguInTerm (Term t1, Term t2, int (*iterator) ())
|
|||||||
*/
|
*/
|
||||||
int
|
int
|
||||||
termMguSubTerm (Term t1, Term t2, int (*iterator) (),
|
termMguSubTerm (Term t1, Term t2, int (*iterator) (),
|
||||||
const Termlist inverses, Termlist keylist)
|
Termlist inverses, Termlist keylist)
|
||||||
{
|
{
|
||||||
int flag;
|
int flag;
|
||||||
Termlist tl;
|
Termlist tl;
|
||||||
@ -230,8 +230,8 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (),
|
|||||||
|
|
||||||
// Recurse
|
// Recurse
|
||||||
flag =
|
flag =
|
||||||
flag & termMguSubTerm (t1, t2->left.op, iterator, inverses,
|
flag && termMguSubTerm (t1, t2->left.op, iterator, inverses,
|
||||||
keylist_new);
|
keylist_new);
|
||||||
|
|
||||||
termlistDelete (keylist_new);
|
termlistDelete (keylist_new);
|
||||||
termDelete (newkey);
|
termDelete (newkey);
|
||||||
@ -242,7 +242,7 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (),
|
|||||||
if (tl != MGUFAIL)
|
if (tl != MGUFAIL)
|
||||||
{
|
{
|
||||||
// Iterate
|
// Iterate
|
||||||
flag = flag & iterator (tl, keylist);
|
flag = flag && iterator (tl, keylist);
|
||||||
// Reset variables
|
// Reset variables
|
||||||
termlistSubstReset (tl);
|
termlistSubstReset (tl);
|
||||||
}
|
}
|
||||||
|
@ -17,7 +17,7 @@
|
|||||||
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) ());
|
||||||
int termMguSubTerm (Term t1, Term t2, int (*iterator) (),
|
int termMguSubTerm (Term t1, Term t2, int (*iterator) (),
|
||||||
const Termlist inverses, Termlist keylist);
|
Termlist inverses, Termlist keylist);
|
||||||
void termlistSubstReset (Termlist tl);
|
void termlistSubstReset (Termlist tl);
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
Loading…
Reference in New Issue
Block a user