andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Niagree claim seems to be working fine now.

Browse Source
This commit is contained in:
ccremers 2004-08-27 17:25:38 +00:00
parent 2decf44bd2
commit 21b2c27320
2 changed files with 52 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
src/arachne.c
View File

@ -1329,7 +1329,7 @@ prune_claim_specifics ()
{
if (current_claim->type == CLAIM_Niagree)
{
if (arachne_claim_niagree (sys, current_claim->r, current_claim->ev))
if (arachne_claim_niagree (sys, 0, current_claim->ev))
{
current_claim->count = statesIncrease (current_claim->count);
if (sys->output == PROOF)
@ -1342,7 +1342,7 @@ prune_claim_specifics ()
}
if (current_claim->type == CLAIM_Nisynch)
{
if (arachne_claim_nisynch (sys, current_claim->r, current_claim->ev))
if (arachne_claim_nisynch (sys, 0, current_claim->ev))
{
current_claim->count = statesIncrease (current_claim->count);
if (sys->output == PROOF)
@ -1402,16 +1402,14 @@ property_check ()
int flag;
flag = 1;
if (current_claim->type == CLAIM_Secret)
{
// Secrecy claim
/**
* By the way the claim is handled, this automatically means a flaw.
*/
count_false ();
if (sys->output == ATTACK)
printSemiState ();
}
/**
* By the way the claim is handled, this automatically means a flaw.
*/
count_false ();
if (sys->output == ATTACK)
printSemiState ();
return flag;
}

46
src/claim.c
View File

@ -3,6 +3,7 @@
#include "system.h"
#include "label.h"
#include "error.h"
#include "debug.h"
#define MATCH_NONE 0
#define MATCH_ORDER 1
@ -12,6 +13,8 @@
#define LABEL_GOOD -3
#define LABEL_TODO -2
extern int globalError;
// Debugging the NI-SYNCH checks
//#define OKIDEBUG
@ -477,6 +480,15 @@ int arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs
Termlist labels;
int flag;
#ifdef DEBUG
if (DEBUGL (5))
{
eprintf ("Checking runs agreement for Arachne.\n");
termmapPrint (runs);
eprintf ("\n");
}
#endif
flag = 1;
labels = cl->prec;
while (flag && labels != NULL)
@ -492,7 +504,25 @@ int arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs
int i;
int run;
run = termmapGet (runs, label);
run = termmapGet (runs, role);
#ifdef DEBUG
if (run < 0 || run >= sys->maxruns )
{
globalError++;
eprintf ("Run mapping %i out of bounds for role ", run);
termPrint (role);
eprintf (" and label ");
termPrint (label);
eprintf ("\n");
eprintf ("This label has sendrole ");
termPrint (linfo->sendrole);
eprintf (" and readrole ");
termPrint (linfo->readrole);
eprintf ("\n");
globalError--;
error ("Run mapping is out of bounds.");
}
#endif
rd = sys->runs[run].start;
rd_res = NULL;
i = 0;
@ -559,11 +589,12 @@ int arachne_claim_niagree (const System sys, const int claim_run, const int clai
else
{
// Choose a run for this role, if possible
// Note that any will do
int run, flag;
run = 0;
flag = 1;
while (flag && run < sys->maxruns)
flag = 0;
while (run < sys->maxruns)
{
// Has to be from the right protocol
if (sys->runs[run].protocol == cl->protocol)
@ -573,7 +604,7 @@ int arachne_claim_niagree (const System sys, const int claim_run, const int clai
{
// Choose, iterate
runs_involved = termmapSet (runs_involved, roles_tofill->term, run);
flag = flag && fill_roles (roles_tofill->next);
flag = flag || fill_roles (roles_tofill->next);
}
}
run++;
@ -582,6 +613,13 @@ int arachne_claim_niagree (const System sys, const int claim_run, const int clai
}
}
#ifdef DEBUG
if (DEBUGL (5))
{
eprintf ("Testing for Niagree claim with any sort of runs.\n");
}
#endif
rd = roledef_shift (sys->runs[claim_run].start, claim_index);
#ifdef DEBUG
if (rd == NULL)