From 45d5cb0a3aa24c5288d89f2c84433ae25bd11ebe Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Wed, 19 Jun 2013 21:51:52 +0200 Subject: [PATCH] Cleanup: Cleanup of some spacing, conform coding conventions. This is simply the result from running reindent.sh again. --- src/arachne.c | 58 ++++++++++++++++++++++---------------------- src/compiler.c | 29 ++++++++++++---------- src/prune_theorems.c | 12 +++++---- src/tac.c | 4 +-- src/tac.h | 2 +- 5 files changed, 55 insertions(+), 50 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index d6bca88..932feff 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -1086,48 +1086,48 @@ bind_new_run (const Binding b, const Protocol p, const Role r, //! Proof markers void -proof_go_down(const Term label, const Term t) +proof_go_down (const Term label, const Term t) { Termlist l; int depth; int len; if (switches.output != PROOF) - return; + return; // Prepend the terms (the list is in reverse) - TERMLISTPREPEND(sys->proofstate,label); - TERMLISTPREPEND(sys->proofstate,t); - len = termlistLength(sys->proofstate) / 2; + TERMLISTPREPEND (sys->proofstate, label); + TERMLISTPREPEND (sys->proofstate, t); + len = termlistLength (sys->proofstate) / 2; // Display state - eprintf("Proof state: branch at level %i\n", len); - l = termlistForward(sys->proofstate); + eprintf ("Proof state: branch at level %i\n", len); + l = termlistForward (sys->proofstate); depth = 0; while (l != NULL) { int i; - eprintf("Proof state: "); + eprintf ("Proof state: "); for (i = 0; i < depth; i++) { - eprintf(" "); + eprintf (" "); } - termPrint(l->prev->term); - eprintf("("); - termPrint(l->term); - eprintf("); "); + termPrint (l->prev->term); + eprintf ("("); + termPrint (l->term); + eprintf ("); "); l = l->prev->prev; - eprintf("\n"); + eprintf ("\n"); depth++; } } void -proof_go_up(void) +proof_go_up (void) { if (switches.output != PROOF) - return; - sys->proofstate = termlistDelTerm(sys->proofstate); - sys->proofstate = termlistDelTerm(sys->proofstate); + return; + sys->proofstate = termlistDelTerm (sys->proofstate); + sys->proofstate = termlistDelTerm (sys->proofstate); return; } @@ -1429,16 +1429,16 @@ bind_goal_regular_run (const Binding b) #ifdef DEBUG debug (5, "Trying to bind to existing run."); #endif - proof_go_down(TERM_DeEx,b->term); + proof_go_down (TERM_DeEx, b->term); sflag = bind_existing_run (b, p, r, index); - proof_go_up(); + proof_go_up (); // bind to new run #ifdef DEBUG debug (5, "Trying to bind to new run."); #endif - proof_go_down(TERM_DeNew,b->term); + proof_go_down (TERM_DeNew, b->term); sflag = sflag && bind_new_run (b, p, r, index); - proof_go_up(); + proof_go_up (); indentDepth--; return sflag; @@ -1634,21 +1634,21 @@ bind_goal_all_options (const Binding b) if (know_only) { // Special case: only from intruder - proof_go_down(TERM_CoOld,b->term); + proof_go_down (TERM_CoOld, b->term); flag = flag && bind_goal_old_intruder_run (b); //flag = flag && bind_goal_new_intruder_run (b); - proof_go_up(); + proof_go_up (); } else { // Normal case - flag = bind_goal_regular_run (b); - proof_go_down(TERM_CoOld,b->term); + flag = bind_goal_regular_run (b); + proof_go_down (TERM_CoOld, b->term); flag = flag && bind_goal_old_intruder_run (b); - proof_go_up(); - proof_go_down(TERM_CoNew,b->term); + proof_go_up (); + proof_go_down (TERM_CoNew, b->term); flag = flag && bind_goal_new_intruder_run (b); - proof_go_up(); + proof_go_up (); } proofDepth--; diff --git a/src/compiler.c b/src/compiler.c index ae50de5..2dc95a6 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -790,30 +790,32 @@ matchEvent (Tac tc) Labelinfo linfo; /* Create fresh Nonce variable */ - nsymb = symbolNextFree(TermSymb(TERM_Hidden)); - tvar = symbolDeclare(nsymb,false); + nsymb = symbolNextFree (TermSymb (TERM_Hidden)); + tvar = symbolDeclare (nsymb, false); //tvar->stype = termlistAdd(NULL,TERM_Nonce); /* Make the concrete messages */ mpat = tacTerm (tc->t1.tac); mmsg = tacTerm (tc->t2.tac); - msg1 = makeTermEncrypt(mmsg,tvar); - msg2 = makeTermEncrypt(mpat,tvar); + msg1 = makeTermEncrypt (mmsg, tvar); + msg2 = makeTermEncrypt (mpat, tvar); /* Declare the const */ - thisRole->declaredconsts = termlistAdd(thisRole->declaredconsts, tvar); + thisRole->declaredconsts = termlistAdd (thisRole->declaredconsts, tvar); /* And send & recv combo (implementing the syntactic sugar) */ - label1 = freshTermPrefix(LABEL_Match); + label1 = freshTermPrefix (LABEL_Match); linfo = label_create (label1, thisProtocol); sys->labellist = list_append (sys->labellist, linfo); myrole = thisRole->nameterm; /* add send event */ - thisRole->roledef = roledefAdd (thisRole->roledef, SEND, label1, myrole, myrole, msg1, NULL); + thisRole->roledef = + roledefAdd (thisRole->roledef, SEND, label1, myrole, myrole, msg1, NULL); markLastRoledef (thisRole->roledef, tc->lineno); /* add recv event */ - thisRole->roledef = roledefAdd (thisRole->roledef, RECV, label1, myrole, myrole, msg2, NULL); + thisRole->roledef = + roledefAdd (thisRole->roledef, RECV, label1, myrole, myrole, msg2, NULL); markLastRoledef (thisRole->roledef, tc->lineno); } @@ -834,8 +836,9 @@ nonMatchEvent (Tac tc) mpat = tacTerm (tc->t1.tac); mmsg = tacTerm (tc->t2.tac); - msg = makeTermTuple(mpat,mmsg); - claimCreate (sys, thisProtocol, thisRole, CLAIM_Notequal, NULL, msg, tc->lineno); + msg = makeTermTuple (mpat, mmsg); + claimCreate (sys, thisProtocol, thisRole, CLAIM_Notequal, NULL, msg, + tc->lineno); } //! Parse a communication event tc of type event, and add a role definition event for it. @@ -1272,11 +1275,11 @@ roleCompile (Term nameterm, Tac tc) case TAC_MATCH: if (tc->t3.value == true) { - matchEvent (tc); + matchEvent (tc); } - else + else { - nonMatchEvent (tc); + nonMatchEvent (tc); } break; case TAC_CLAIM: diff --git a/src/prune_theorems.c b/src/prune_theorems.c index d676027..104602e 100644 --- a/src/prune_theorems.c +++ b/src/prune_theorems.c @@ -204,22 +204,24 @@ inequalityConstraints (const System sys) Roledef rd; rd = sys->runs[run].start; - for (e = 0; e < sys->runs[run].step; e++) + for (e = 0; e < sys->runs[run].step; e++) { if (rd->type == CLAIM) { // It's a claim - if (isTermEqual (rd->claiminfo->type, CLAIM_Notequal)) + if (isTermEqual (rd->claiminfo->type, CLAIM_Notequal)) { // TODO ASSERT: Message should be a pair for NotEqual claims - if (isTermEqual (TermOp1(rd->message),TermOp2(rd->message))) + if (isTermEqual + (TermOp1 (rd->message), TermOp2 (rd->message))) { // Inequality violated, no solution exists that makes them inequal anymore. if (switches.output == PROOF) { indentPrint (); - eprintf ("Pruned because the pattern violates an inequality constraint based on the term "); - termPrint (TermOp1(rd->message)); + eprintf + ("Pruned because the pattern violates an inequality constraint based on the term "); + termPrint (TermOp1 (rd->message)); eprintf (".\n"); } diff --git a/src/tac.c b/src/tac.c index 84bc1df..38283fd 100644 --- a/src/tac.c +++ b/src/tac.c @@ -53,8 +53,8 @@ tacDone (void) } //! Copy a tac -Tac -tacCopy(Tac c) +Tac +tacCopy (Tac c) { Tac newTac; diff --git a/src/tac.h b/src/tac.h index 2d303d1..cba8998 100644 --- a/src/tac.h +++ b/src/tac.h @@ -93,7 +93,7 @@ typedef struct tacnode *Tac; void tacInit (void); void tacDone (void); -Tac tacCopy(Tac c); +Tac tacCopy (Tac c); Tac tacCreate (int op); Tac tacSymb (char *s); Tac tacJoin (int op, Tac t1, Tac t2, Tac t3);