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

- Fixed bug where claim fails were not counted in the modelchecker, as

Browse Source 
reported bij GH. Attacks were indicated, though, so this only caused
  problems for users using --summary and not looking at the "attack:
  L:?" field.
This commit is contained in:
ccremers 2005-04-27 11:43:47 +00:00
parent b00cabe35a
commit 7c0507a900
1 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/modelchecker.c
View File

@ -1233,12 +1233,15 @@ int
violateClaim (const System sys, int length, int claimev, Termlist reqt) violateClaim (const System sys, int length, int claimev, Termlist reqt)
{ {
int flag; int flag;
Claimlist clinfo;
/* default = no adaption of pruning, continue search */ /* default = no adaption of pruning, continue search */
flag = 1; flag = 1;
/* Count the violations */ /* Count the violations */
sys->failed = statesIncrease (sys->failed); sys->failed = statesIncrease (sys->failed);
clinfo = sys->traceEvent[claimev]->claiminfo;
clinfo->failed = statesIncrease (clinfo->failed); // note: for modelchecking secrecy, this can lead to more fails (at further events in branches of the tree) than claim encounters
/* mark the path in the state graph? */ /* mark the path in the state graph? */
if (sys->output == STATESPACE) if (sys->output == STATESPACE)