diff --git a/src/arachne.c b/src/arachne.c index 1868435..918b111 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -662,10 +662,10 @@ iterate_role_sends (int (*func) ()) index = 0; while (rd != NULL) { - if (rd->type == SEND) + if (rd->type == SEND) { if (!func (p, r, rd, index)) - return 0; + return 0; } index++; rd = rd->next; diff --git a/src/binding.c b/src/binding.c index 1be64ff..14b1db8 100644 --- a/src/binding.c +++ b/src/binding.c @@ -195,7 +195,7 @@ goal_unbind (const Binding b) //! Check if term,run,ev already occurs in binding 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; @@ -252,7 +252,7 @@ goal_add (Term term, const int run, const int ev, const int level) else { // Determine whether we already had it - if (is_new_binding(term, run, ev)) + if (is_new_binding (term, run, ev)) { // Add a new binding Binding b; @@ -424,7 +424,7 @@ iterate_preceding_bindings (const int run, const int ev, b = (Binding) bl->data; if (isDependEvent (b->run_to, b->ev_to, run, ev)) { - if (!func (b)) + if (!func (b)) { return false; } @@ -640,9 +640,9 @@ countBindingsDone () b = (Binding) bl->data; if ((!b->blocked) && b->done) - { + { count++; - } + } } return count; } diff --git a/src/compiler.c b/src/compiler.c index 46b6b4e..39bb495 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -131,11 +131,11 @@ compute_recv_variables (const Role r) while (rd != NULL) { if (rd->type == RECV) - { + { tl = termlistAddVariables (tl, rd->from); tl = termlistAddVariables (tl, rd->to); tl = termlistAddVariables (tl, rd->message); - } + } rd = rd->next; } return tl; diff --git a/src/dotout.c b/src/dotout.c index b1e84e2..884ff7c 100644 --- a/src/dotout.c +++ b/src/dotout.c @@ -726,7 +726,9 @@ isApplicationM0 (const System sys, const int run) * Name & documentation might be off; TODO later. * 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 @@ -738,11 +740,10 @@ int preceventPossible (const System sys, const int rank, const int run, const in if (rank2 == rank) { // equal rank: only if different run - if ((sys->runs[run].protocol != INTRUDER) - && (run2 == run)) - { - return false; - } + if ((sys->runs[run].protocol != INTRUDER) && (run2 == run)) + { + return false; + } } 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. */ 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; @@ -767,7 +769,7 @@ iteratePrecedingRole(const System sys, const int *ranks, const int run, const in { int rank2; - rank2 = ranks[eventNode (run2, ev2)]; + rank2 = ranks[eventNode (run2, ev2)]; if (!preceventPossible (sys, rank, run, rank2, run2, ev2)) { return false; @@ -823,32 +825,32 @@ graph_ranks (int *ranks, int nodes) changes = false; for (run = 0; run < sys->maxruns; run++) - { - Roledef rd; - int ev; + { + Roledef rd; + int ev; - rd = sys->runs[run].start; - 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 + rd = sys->runs[run].start; + 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 ( ranks[eventNode (run, ev)] == INT_MAX) - { - if (iteratePrecedingRole (sys, ranks, run, ev, rank)) - { - // we can do it! - changes = true; - ranks[eventNode (run, ev)] = rank; - } - else - { - done = false; - } - } - rd = rd->next; + if (ranks[eventNode (run, ev)] == INT_MAX) + { + if (iteratePrecedingRole (sys, ranks, run, ev, rank)) + { + // we can do it! + changes = true; + ranks[eventNode (run, ev)] = rank; + } + else + { + done = false; + } + } + rd = rd->next; } - } - } + } + } } return rank; diff --git a/src/switches.c b/src/switches.c index dc03f6e..c5a2db6 100644 --- a/src/switches.c +++ b/src/switches.c @@ -1703,7 +1703,8 @@ process_switches (int commandline) { printf ("Try '%s --help' for more information, or visit:\n", 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); } else diff --git a/src/system.c b/src/system.c index a8e21bd..0f22aa0 100644 --- a/src/system.c +++ b/src/system.c @@ -455,13 +455,13 @@ run_localize (const System sys, const int rid, Termlist fromlist, t = substlist->term; if (t != NULL) { - if (t->subst != NULL) - { - t->subst = termLocal (t->subst, fromlist, tolist); - sys->runs[rid].substitutions = - termlistAdd (sys->runs[rid].substitutions, t); - } - } + if (t->subst != NULL) + { + t->subst = termLocal (t->subst, fromlist, tolist); + sys->runs[rid].substitutions = + termlistAdd (sys->runs[rid].substitutions, t); + } + } substlist = substlist->next; } } diff --git a/src/termlist.c b/src/termlist.c index 0f70edc..57900a5 100644 --- a/src/termlist.c +++ b/src/termlist.c @@ -636,7 +636,7 @@ termLocal (const Term tPre, Termlist fromlist, Termlist tolist) if (tPre == NULL) return NULL; - t = deVar(tPre); + t = deVar (tPre); if (realTermLeaf (t)) { @@ -655,7 +655,7 @@ termLocal (const Term tPre, Termlist fromlist, Termlist tolist) else { Term newt; - + newt = termNodeDuplicate (t); if (realTermTuple (t)) { diff --git a/src/xmlout.c b/src/xmlout.c index 394d029..a41a5fb 100644 --- a/src/xmlout.c +++ b/src/xmlout.c @@ -539,13 +539,15 @@ isEventInteresting (const System sys, const Roledef rd) } //! 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); } //! Refactoring code from below -void xmlShowThisBinding(const Binding b) +void +xmlShowThisBinding (const Binding b) { 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 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; 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--; }