Introduced '-c,--characterize' switches for complete characterization.
This switch was previously known as '--state-space', but the new name is much better. Backwards compatibility: '-c' was previously used by '--check', so check is now abbreviated to '-C'. '-s,--state-space' still works but is from now on considered to be deprecated.
This commit is contained in:
parent
b02c09f0dd
commit
2d45daa8ee
@ -550,12 +550,14 @@ switcher (const int process, int index, int commandline)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
if (detect ('c', "check", 0))
|
if (detect ('C', "check", 0))
|
||||||
{
|
{
|
||||||
if (!process)
|
if (!process)
|
||||||
{
|
{
|
||||||
helptext ("-c, --check",
|
/* discourage: not working well currently.
|
||||||
|
helptext ("-C, --check",
|
||||||
"disable intruder and run statespace check. For correct protocols, end of roles should be reachable");
|
"disable intruder and run statespace check. For correct protocols, end of roles should be reachable");
|
||||||
|
*/
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
@ -599,14 +601,17 @@ switcher (const int process, int index, int commandline)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
if (detect ('s', "state-space", 0))
|
if (detect ('c', "characterize", 0) || detect ('s', "state-space", 0))
|
||||||
{
|
{
|
||||||
|
/*
|
||||||
|
* TODO maybe this switch should also filter out the intruder.
|
||||||
|
*/
|
||||||
if (!process)
|
if (!process)
|
||||||
{
|
{
|
||||||
if (switches.expert)
|
if (switches.expert)
|
||||||
{
|
{
|
||||||
helptext ("-s, --state-space",
|
helptext ("-c, --characterize",
|
||||||
"ignore any existing claims and add 'reachable' claims. Gives complete characterization of a roles");
|
"Ignore claims and give complete characterization of all roles");
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
|
Loading…
Reference in New Issue
Block a user