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

- Modified -l switch to also serve as proof depth limit.

Browse Source
This commit is contained in:
ccremers 2004-10-14 15:25:28 +00:00
parent ba832159b1
commit d33ec486ce
2 changed files with 16 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
src/arachne.c
View File

@ -48,6 +48,7 @@ Role I_D;
Role I_RRS; Role I_RRS;
static int indentDepth; static int indentDepth;
static int proofDepth;
static int max_encryption_level; static int max_encryption_level;
static int num_regular_runs; static int num_regular_runs;
static int num_intruder_runs; static int num_intruder_runs;
@ -1445,6 +1446,7 @@ bind_goal (const Binding b)
} }
} }
proofDepth++;
if (know_only) if (know_only)
{ {
// Special case: only from intruder // Special case: only from intruder
@ -1458,6 +1460,7 @@ bind_goal (const Binding b)
flag = flag && bind_goal_old_intruder_run (b); flag = flag && bind_goal_old_intruder_run (b);
flag = flag && bind_goal_new_intruder_run (b); flag = flag && bind_goal_new_intruder_run (b);
} }
proofDepth--;
indentDepth--; indentDepth--;
return flag; return flag;
@ -1664,6 +1667,17 @@ prune_bounds ()
Termlist tl; Termlist tl;
List bl; List bl;
if (proofDepth > sys->switch_maxtracelength)
{
// Hardcoded limit on proof tree depth
if (sys->output == PROOF)
{
indentPrint ();
eprintf ("Pruned: proof tree too deep: %i (-l %i switch)\n", proofDepth, sys->switch_maxtracelength);
}
return 1;
}
if (num_regular_runs > sys->switchRuns) if (num_regular_runs > sys->switchRuns)
{ {
// Hardcoded limit on runs // Hardcoded limit on runs
@ -1949,6 +1963,7 @@ arachne ()
#endif #endif
indentDepth = 0; indentDepth = 0;
proofDepth = 0;
cl = sys->claimlist; cl = sys->claimlist;
while (cl != NULL) while (cl != NULL)
{ {

2
src/main.c
View File

@ -113,7 +113,7 @@ main (int argc, char **argv)
"pruning method (default is 2)"); "pruning method (default is 2)");
struct arg_int *switch_prune_trace_length = struct arg_int *switch_prune_trace_length =
arg_int0 ("l", "max-length", NULL, arg_int0 ("l", "max-length", NULL,
"prune traces longer than <int> events"); "prune traces longer than <int> events, prune proof deeper than <int> splits.");
struct arg_lit *switch_incremental_trace_length = struct arg_lit *switch_incremental_trace_length =
arg_lit0 (NULL, "increment-traces", arg_lit0 (NULL, "increment-traces",
"incremental search using the length of the traces."); "incremental search using the length of the traces.");