Removed a slightly more complex trampoline by making a stateful iterator.
This commit is contained in:
parent
4748d2f4d2
commit
b6f4fcbb7a
@ -61,6 +61,12 @@
|
|||||||
#include "heuristic.h"
|
#include "heuristic.h"
|
||||||
#include "tempfile.h"
|
#include "tempfile.h"
|
||||||
|
|
||||||
|
struct brsstate
|
||||||
|
{
|
||||||
|
Binding binding;
|
||||||
|
int found;
|
||||||
|
};
|
||||||
|
|
||||||
extern int *graph;
|
extern int *graph;
|
||||||
extern int nodes;
|
extern int nodes;
|
||||||
extern int graph_uordblks;
|
extern int graph_uordblks;
|
||||||
@ -1520,22 +1526,11 @@ process_good_candidate (const Protocol p, const Role r, const Roledef rd,
|
|||||||
return sflag;
|
return sflag;
|
||||||
}
|
}
|
||||||
|
|
||||||
//! Bind a regular goal
|
//! Helper for the next function bind_regular_goal
|
||||||
/**
|
|
||||||
* Problem child. Valgrind does not like it.
|
|
||||||
*/
|
|
||||||
int
|
int
|
||||||
bind_goal_regular_run (const Binding b)
|
bind_this_role_send (Protocol p, Role r, Roledef rd, int index,
|
||||||
|
struct brsstate *bs)
|
||||||
{
|
{
|
||||||
int flag;
|
|
||||||
int found;
|
|
||||||
|
|
||||||
/*
|
|
||||||
* This is a local function so we have access to goal
|
|
||||||
*/
|
|
||||||
int bind_this_role_send (Protocol p, Role r, Roledef rd, int index,
|
|
||||||
void *state)
|
|
||||||
{
|
|
||||||
if (p == INTRUDER)
|
if (p == INTRUDER)
|
||||||
{
|
{
|
||||||
// No intruder roles here
|
// No intruder roles here
|
||||||
@ -1546,24 +1541,36 @@ bind_goal_regular_run (const Binding b)
|
|||||||
debug_send_candidate (p, r, rd, index);
|
debug_send_candidate (p, r, rd, index);
|
||||||
|
|
||||||
if (!subtermUnify
|
if (!subtermUnify
|
||||||
(rd->message, b->term, NULL, NULL, test_sub_unification))
|
(rd->message, (bs->binding)->term, NULL, NULL, test_sub_unification))
|
||||||
{
|
{
|
||||||
// A good candidate
|
// A good candidate
|
||||||
found++;
|
bs->found++;
|
||||||
return process_good_candidate (p, r, rd, index, b, found);
|
return process_good_candidate (p, r, rd, index, bs->binding, bs->found);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
//! Bind a regular goal
|
||||||
|
/**
|
||||||
|
* Problem child. Valgrind did not like it.
|
||||||
|
* TODO maybe better since last rewrite; need to check again.
|
||||||
|
*/
|
||||||
|
int
|
||||||
|
bind_goal_regular_run (const Binding b)
|
||||||
|
{
|
||||||
|
int flag;
|
||||||
|
struct brsstate bs;
|
||||||
|
|
||||||
// Bind to all possible sends of regular runs
|
// Bind to all possible sends of regular runs
|
||||||
found = 0;
|
bs.found = 0;
|
||||||
flag = iterate_state_role_sends (bind_this_role_send, NULL);
|
bs.binding = b;
|
||||||
|
|
||||||
proof_term_match_none (b, found);
|
flag = iterate_state_role_sends (bind_this_role_send, &bs);
|
||||||
|
|
||||||
|
proof_term_match_none (b, bs.found);
|
||||||
return flag;
|
return flag;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user