- Added '--extend-nonreads' switch. It is totally untested, and I hope
Gijs will have a look at it and tell me whether it actually works.
This commit is contained in:
parent
b6e9841c0f
commit
464920907b
@ -73,9 +73,11 @@ switchesInit (int argc, char **argv)
|
|||||||
switches.reportClaims = 0; // default don't report on claims
|
switches.reportClaims = 0; // default don't report on claims
|
||||||
switches.xml = 0; // default no xml output
|
switches.xml = 0; // default no xml output
|
||||||
switches.human = false; // not human friendly by default
|
switches.human = false; // not human friendly by default
|
||||||
switches.reportMemory;
|
switches.reportMemory = 0;
|
||||||
switches.reportTime;
|
switches.reportTime = 0;
|
||||||
switches.reportStates;
|
switches.reportStates = 0;
|
||||||
|
switches.extendNonReads = 0; // default off
|
||||||
|
|
||||||
// Obsolete
|
// Obsolete
|
||||||
switches.latex = 0; // latex output?
|
switches.latex = 0; // latex output?
|
||||||
|
|
||||||
@ -449,6 +451,20 @@ switcher (const int process, int index)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
if (detect (' ', "extend-nonreads", 0))
|
||||||
|
{
|
||||||
|
if (!process)
|
||||||
|
{
|
||||||
|
/* discourage: hide
|
||||||
|
*/
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
switches.extendNonReads = 1;
|
||||||
|
return index;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
/* ==================
|
/* ==================
|
||||||
* External options
|
* External options
|
||||||
*/
|
*/
|
||||||
|
@ -55,6 +55,8 @@ struct switchdata
|
|||||||
int reportMemory; //!< Memory display switch.
|
int reportMemory; //!< Memory display switch.
|
||||||
int reportTime; //!< Time display switch.
|
int reportTime; //!< Time display switch.
|
||||||
int reportStates; //!< Progress display switch. (traversed states)
|
int reportStates; //!< Progress display switch. (traversed states)
|
||||||
|
int extendNonReads; //!< Show further events in arachne xml output.
|
||||||
|
|
||||||
//! Latex output switch.
|
//! Latex output switch.
|
||||||
/**
|
/**
|
||||||
* Obsolete. Use globalLatex instead.
|
* Obsolete. Use globalLatex instead.
|
||||||
|
32
src/xmlout.c
32
src/xmlout.c
@ -711,9 +711,36 @@ xmlOutRuns (const System sys)
|
|||||||
Roledef rd;
|
Roledef rd;
|
||||||
int index;
|
int index;
|
||||||
|
|
||||||
|
//! Test whether to display this event
|
||||||
|
/**
|
||||||
|
* Could be integrated into a single line on the while loop,
|
||||||
|
* but that makes it rather hard to understand.
|
||||||
|
*/
|
||||||
|
int showthis (void)
|
||||||
|
{
|
||||||
|
if (rd != NULL)
|
||||||
|
{
|
||||||
|
if (index < sys->runs[run].step)
|
||||||
|
{
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
if (switches.extendNonReads)
|
||||||
|
{
|
||||||
|
if (rd->type != READ)
|
||||||
|
{
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
|
||||||
index = 0;
|
index = 0;
|
||||||
rd = sys->runs[run].start;
|
rd = sys->runs[run].start;
|
||||||
while (rd != NULL && index < sys->runs[run].step)
|
while (showthis ())
|
||||||
{
|
{
|
||||||
xmlOutEvent (sys, rd, run, index);
|
xmlOutEvent (sys, rd, run, index);
|
||||||
index++;
|
index++;
|
||||||
@ -752,6 +779,9 @@ xmlOutSemitrace (const System sys)
|
|||||||
xmlIndentPrint ();
|
xmlIndentPrint ();
|
||||||
printf ("<attack");
|
printf ("<attack");
|
||||||
/* add trace length attribute */
|
/* add trace length attribute */
|
||||||
|
/* Note that this is the length of the attack leading up to the broken
|
||||||
|
* claim, thus without any run extensions (--extend-nonreads).
|
||||||
|
*/
|
||||||
printf (" tracelength=\"%i\"", get_semitrace_length ());
|
printf (" tracelength=\"%i\"", get_semitrace_length ());
|
||||||
/* add attack id attribute (within this scyther call) */
|
/* add attack id attribute (within this scyther call) */
|
||||||
printf (" id=\"%i\"", sys->attackid);
|
printf (" id=\"%i\"", sys->attackid);
|
||||||
|
Loading…
Reference in New Issue
Block a user