Reindent code for consistency.
This commit is contained in:
parent
369ae1e3f8
commit
0d9c23c33b
@ -662,10 +662,10 @@ iterate_role_sends (int (*func) ())
|
|||||||
index = 0;
|
index = 0;
|
||||||
while (rd != NULL)
|
while (rd != NULL)
|
||||||
{
|
{
|
||||||
if (rd->type == SEND)
|
if (rd->type == SEND)
|
||||||
{
|
{
|
||||||
if (!func (p, r, rd, index))
|
if (!func (p, r, rd, index))
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
index++;
|
index++;
|
||||||
rd = rd->next;
|
rd = rd->next;
|
||||||
|
@ -195,7 +195,7 @@ goal_unbind (const Binding b)
|
|||||||
|
|
||||||
//! Check if term,run,ev already occurs in binding
|
//! Check if term,run,ev already occurs in binding
|
||||||
int
|
int
|
||||||
is_new_binding(const Term term, const int run, const int ev)
|
is_new_binding (const Term term, const int run, const int ev)
|
||||||
{
|
{
|
||||||
List bl = sys->bindings;
|
List bl = sys->bindings;
|
||||||
|
|
||||||
@ -252,7 +252,7 @@ goal_add (Term term, const int run, const int ev, const int level)
|
|||||||
else
|
else
|
||||||
{
|
{
|
||||||
// Determine whether we already had it
|
// Determine whether we already had it
|
||||||
if (is_new_binding(term, run, ev))
|
if (is_new_binding (term, run, ev))
|
||||||
{
|
{
|
||||||
// Add a new binding
|
// Add a new binding
|
||||||
Binding b;
|
Binding b;
|
||||||
@ -424,7 +424,7 @@ iterate_preceding_bindings (const int run, const int ev,
|
|||||||
b = (Binding) bl->data;
|
b = (Binding) bl->data;
|
||||||
if (isDependEvent (b->run_to, b->ev_to, run, ev))
|
if (isDependEvent (b->run_to, b->ev_to, run, ev))
|
||||||
{
|
{
|
||||||
if (!func (b))
|
if (!func (b))
|
||||||
{
|
{
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
@ -640,9 +640,9 @@ countBindingsDone ()
|
|||||||
|
|
||||||
b = (Binding) bl->data;
|
b = (Binding) bl->data;
|
||||||
if ((!b->blocked) && b->done)
|
if ((!b->blocked) && b->done)
|
||||||
{
|
{
|
||||||
count++;
|
count++;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
return count;
|
return count;
|
||||||
}
|
}
|
||||||
|
@ -131,11 +131,11 @@ compute_recv_variables (const Role r)
|
|||||||
while (rd != NULL)
|
while (rd != NULL)
|
||||||
{
|
{
|
||||||
if (rd->type == RECV)
|
if (rd->type == RECV)
|
||||||
{
|
{
|
||||||
tl = termlistAddVariables (tl, rd->from);
|
tl = termlistAddVariables (tl, rd->from);
|
||||||
tl = termlistAddVariables (tl, rd->to);
|
tl = termlistAddVariables (tl, rd->to);
|
||||||
tl = termlistAddVariables (tl, rd->message);
|
tl = termlistAddVariables (tl, rd->message);
|
||||||
}
|
}
|
||||||
rd = rd->next;
|
rd = rd->next;
|
||||||
}
|
}
|
||||||
return tl;
|
return tl;
|
||||||
|
64
src/dotout.c
64
src/dotout.c
@ -726,7 +726,9 @@ isApplicationM0 (const System sys, const int run)
|
|||||||
* Name & documentation might be off; TODO later.
|
* Name & documentation might be off; TODO later.
|
||||||
* This is for now just a refactoring to get rid of trampolines.
|
* This is for now just a refactoring to get rid of trampolines.
|
||||||
*/
|
*/
|
||||||
int preceventPossible (const System sys, const int rank, const int run, const int rank2, const int run2, const int ev2)
|
int
|
||||||
|
preceventPossible (const System sys, const int rank, const int run,
|
||||||
|
const int rank2, const int run2, const int ev2)
|
||||||
{
|
{
|
||||||
// regular preceding event
|
// regular preceding event
|
||||||
|
|
||||||
@ -738,11 +740,10 @@ int preceventPossible (const System sys, const int rank, const int run, const in
|
|||||||
if (rank2 == rank)
|
if (rank2 == rank)
|
||||||
{
|
{
|
||||||
// equal rank: only if different run
|
// equal rank: only if different run
|
||||||
if ((sys->runs[run].protocol != INTRUDER)
|
if ((sys->runs[run].protocol != INTRUDER) && (run2 == run))
|
||||||
&& (run2 == run))
|
{
|
||||||
{
|
return false;
|
||||||
return false;
|
}
|
||||||
}
|
|
||||||
}
|
}
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
@ -753,7 +754,8 @@ int preceventPossible (const System sys, const int rank, const int run, const in
|
|||||||
* This is for now just a refactoring to get rid of trampolines.
|
* This is for now just a refactoring to get rid of trampolines.
|
||||||
*/
|
*/
|
||||||
int
|
int
|
||||||
iteratePrecedingRole(const System sys, const int *ranks, const int run, const int ev, const int rank)
|
iteratePrecedingRole (const System sys, const int *ranks, const int run,
|
||||||
|
const int ev, const int rank)
|
||||||
{
|
{
|
||||||
int run2;
|
int run2;
|
||||||
|
|
||||||
@ -767,7 +769,7 @@ iteratePrecedingRole(const System sys, const int *ranks, const int run, const in
|
|||||||
{
|
{
|
||||||
int rank2;
|
int rank2;
|
||||||
|
|
||||||
rank2 = ranks[eventNode (run2, ev2)];
|
rank2 = ranks[eventNode (run2, ev2)];
|
||||||
if (!preceventPossible (sys, rank, run, rank2, run2, ev2))
|
if (!preceventPossible (sys, rank, run, rank2, run2, ev2))
|
||||||
{
|
{
|
||||||
return false;
|
return false;
|
||||||
@ -823,32 +825,32 @@ graph_ranks (int *ranks, int nodes)
|
|||||||
changes = false;
|
changes = false;
|
||||||
|
|
||||||
for (run = 0; run < sys->maxruns; run++)
|
for (run = 0; run < sys->maxruns; run++)
|
||||||
{
|
{
|
||||||
Roledef rd;
|
Roledef rd;
|
||||||
int ev;
|
int ev;
|
||||||
|
|
||||||
rd = sys->runs[run].start;
|
rd = sys->runs[run].start;
|
||||||
for (ev = 0; ev < sys->runs[run].step; ev++)
|
for (ev = 0; ev < sys->runs[run].step; ev++)
|
||||||
{
|
{
|
||||||
if (rd != NULL) // Shouldn't be needed (step should maintain invariant) but good to be safe
|
if (rd != NULL) // Shouldn't be needed (step should maintain invariant) but good to be safe
|
||||||
{
|
{
|
||||||
if ( ranks[eventNode (run, ev)] == INT_MAX)
|
if (ranks[eventNode (run, ev)] == INT_MAX)
|
||||||
{
|
{
|
||||||
if (iteratePrecedingRole (sys, ranks, run, ev, rank))
|
if (iteratePrecedingRole (sys, ranks, run, ev, rank))
|
||||||
{
|
{
|
||||||
// we can do it!
|
// we can do it!
|
||||||
changes = true;
|
changes = true;
|
||||||
ranks[eventNode (run, ev)] = rank;
|
ranks[eventNode (run, ev)] = rank;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
done = false;
|
done = false;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
rd = rd->next;
|
rd = rd->next;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
return rank;
|
return rank;
|
||||||
|
@ -1703,7 +1703,8 @@ process_switches (int commandline)
|
|||||||
{
|
{
|
||||||
printf ("Try '%s --help' for more information, or visit:\n",
|
printf ("Try '%s --help' for more information, or visit:\n",
|
||||||
progname);
|
progname);
|
||||||
printf (" http://www.cs.ox.ac.uk/people/cas.cremers/scyther/index.html\n");
|
printf
|
||||||
|
(" http://www.cs.ox.ac.uk/people/cas.cremers/scyther/index.html\n");
|
||||||
exit (0);
|
exit (0);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
|
14
src/system.c
14
src/system.c
@ -455,13 +455,13 @@ run_localize (const System sys, const int rid, Termlist fromlist,
|
|||||||
t = substlist->term;
|
t = substlist->term;
|
||||||
if (t != NULL)
|
if (t != NULL)
|
||||||
{
|
{
|
||||||
if (t->subst != NULL)
|
if (t->subst != NULL)
|
||||||
{
|
{
|
||||||
t->subst = termLocal (t->subst, fromlist, tolist);
|
t->subst = termLocal (t->subst, fromlist, tolist);
|
||||||
sys->runs[rid].substitutions =
|
sys->runs[rid].substitutions =
|
||||||
termlistAdd (sys->runs[rid].substitutions, t);
|
termlistAdd (sys->runs[rid].substitutions, t);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
substlist = substlist->next;
|
substlist = substlist->next;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -636,7 +636,7 @@ termLocal (const Term tPre, Termlist fromlist, Termlist tolist)
|
|||||||
if (tPre == NULL)
|
if (tPre == NULL)
|
||||||
return NULL;
|
return NULL;
|
||||||
|
|
||||||
t = deVar(tPre);
|
t = deVar (tPre);
|
||||||
|
|
||||||
if (realTermLeaf (t))
|
if (realTermLeaf (t))
|
||||||
{
|
{
|
||||||
@ -655,7 +655,7 @@ termLocal (const Term tPre, Termlist fromlist, Termlist tolist)
|
|||||||
else
|
else
|
||||||
{
|
{
|
||||||
Term newt;
|
Term newt;
|
||||||
|
|
||||||
newt = termNodeDuplicate (t);
|
newt = termNodeDuplicate (t);
|
||||||
if (realTermTuple (t))
|
if (realTermTuple (t))
|
||||||
{
|
{
|
||||||
|
16
src/xmlout.c
16
src/xmlout.c
@ -539,13 +539,15 @@ isEventInteresting (const System sys, const Roledef rd)
|
|||||||
}
|
}
|
||||||
|
|
||||||
//! Refactoring code from below
|
//! Refactoring code from below
|
||||||
void xmlRunIndex (char *desc, const int run, const int index)
|
void
|
||||||
|
xmlRunIndex (char *desc, const int run, const int index)
|
||||||
{
|
{
|
||||||
xmlPrint ("<%s run=\"%i\" index=\"%i\" />", desc, run, index);
|
xmlPrint ("<%s run=\"%i\" index=\"%i\" />", desc, run, index);
|
||||||
}
|
}
|
||||||
|
|
||||||
//! Refactoring code from below
|
//! Refactoring code from below
|
||||||
void xmlShowThisBinding(const Binding b)
|
void
|
||||||
|
xmlShowThisBinding (const Binding b)
|
||||||
{
|
{
|
||||||
if (isTermVariable (b->term) && !b->done)
|
if (isTermVariable (b->term) && !b->done)
|
||||||
{
|
{
|
||||||
@ -647,18 +649,18 @@ xmlOutEvent (const System sys, Roledef rd, const int run, const int index)
|
|||||||
// Only if real run, and not a roledef
|
// Only if real run, and not a roledef
|
||||||
if (run >= 0)
|
if (run >= 0)
|
||||||
{
|
{
|
||||||
List bl;
|
List bl;
|
||||||
|
|
||||||
for (bl = sys->bindings; bl != NULL; bl = bl->next)
|
for (bl = sys->bindings; bl != NULL; bl = bl->next)
|
||||||
{
|
{
|
||||||
Binding b;
|
Binding b;
|
||||||
|
|
||||||
b = (Binding) bl->data;
|
b = (Binding) bl->data;
|
||||||
if (b->run_to == run && b->ev_to == index)
|
if (b->run_to == run && b->ev_to == index)
|
||||||
{
|
{
|
||||||
xmlShowThisBinding(b);
|
xmlShowThisBinding (b);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
xmlindent--;
|
xmlindent--;
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user