The script runs over all protocol files it can find, and runs it using two different
command-line parameters to scyther. If the results differ, the script reports it.
The code can use some cleanup, removing e.g. global variables, but it works.
Reported by ETH students last year: if you include a file, where the file has an
error in a line with a number higher than the original, the Python code crashes.
This is a *patch* only because the real underlying problem is that error reporting
does not take include commands into account, and does not propagate any
file names.
Passing the '--all-attacks' switch to the backend was not working. The reason
was the hack to get Vista working hardcoded cutting to the last attack found.
In the long term, this needs to be cleaned up, and cutting should be moved back
nicely to the Scyther C code where it used to work. Once done, switches.useAttackBuffer
can be set back to true.
BUGFIX: When cutting attacks/patterns, counts are no longer exact.
In the near future, the default exit code behavior should be made obsolete anyway,
as the exit codes are not a nice way to report status.
It used to be convenient for shell scripting in early times,
when the parallel tests were run using the forward model
checker, but no modern script should be relying on it.
When untyped variables occur, the encryption level depth pruning is for
now unjustified. Maybe we can get a proof later. Previously this was
hidden, which was a bad design decision. Now the output is much
clearer.
This cleans up some graphs rather nicely. There is only one potential
drawback (not observed in practive):
If two bindings have the same from/to, but different interpretations,
we might lose information. In particular the 'select' intermediate nodes might
pose a problem and we would be better off by not having any interpretation on
what is selected.
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.
Currently, both my Feisty Ubuntu's have stopped working with the GUI of
Scyther. So to be on the safe side, PIL is disabled for now, until I've
resolved the problem.
The error is the following:
---------------------------------------------------------------------------
Traceback (most recent call last):
File "/home/cas/src/scyther-dev/gui/Gui/Scytherthread.py", line 351, in onViewButton
w = Attackwindow.AttackWindow(btn.claim)
File "/home/cas/src/scyther-dev/gui/Gui/Attackwindow.py", line 176, in __init__
self.CreateInteriorWindowComponents()
File "/home/cas/src/scyther-dev/gui/Gui/Attackwindow.py", line 209, in CreateInteriorWindowComponents
dp = AttackDisplay(self, self, attacks[0])
File "/home/cas/src/scyther-dev/gui/Gui/Attackwindow.py", line 73, in __init__
self.original = Image.open(filename)
File "/usr/lib/python2.5/site-packages/PIL/Image.py", line 1912, in open
return factory(fp, filename)
File "/usr/lib/python2.5/site-packages/PIL/ImageFile.py", line 82, in __init__
self._open()
File "/usr/lib/python2.5/site-packages/PIL/EpsImagePlugin.py", line 277, in _open
raise IOError, "cannot determine EPS bounding box"
IOError: cannot determine EPS bounding box
---------------------------------------------------------------------------
Great. Bounding boxes in eps again.
I've added a marked for the Athena problem case, and now no more false 'complete proof' results are produced.
However, the tool reports, 'no attack within bounds', which is slightly inaccurate
depending on the interpretatio of 'bounds'.
