Cleanup: Cleanup of some spacing, conform coding conventions.
This is simply the result from running reindent.sh again.
This commit is contained in:
Cas Cremers
parent
c6280d745e
commit
45d5cb0a3a
@ -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--;
|
||||
|
||||
|
||||
@ -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
|
||||
{
|
||||
nonMatchEvent (tc);
|
||||
nonMatchEvent (tc);
|
||||
}
|
||||
break;
|
||||
case TAC_CLAIM:
|
||||
|
||||
@ -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");
|
||||
}
|
||||
|
||||
|
||||
@ -54,7 +54,7 @@ tacDone (void)
|
||||
|
||||
//! Copy a tac
|
||||
Tac
|
||||
tacCopy(Tac c)
|
||||
tacCopy (Tac c)
|
||||
{
|
||||
Tac newTac;
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user