Feature #7272
Updated by Evgeny Novikov over 7 years ago
The feature seems useful First time I encountered the following exception: <pre> ... 2016-06-04 14:23:50 (__init__.py:206) ABKM INFO> Verification task decision status is "CPU time exhausted" 2016-06-04 14:23:50 (__init__.py:223) ABKM INFO> Process error trace "output/witness.0.graphml" 2016-06-04 14:23:50 (components.py:101) ABKM ERROR> Raise exception: Traceback (most recent call last): File "/usr/local/lib/python3.4/dist-packages/KleverCore-0.1rc2.dev367_ng322669b-py3.4.egg/core/components.py", line 95, in run self.main() File "/usr/local/lib/python3.4/dist-packages/KleverCore-0.1rc2.dev367_ng322669b-py3.4.egg/core/utils.py", line 38, in callbacks_caller ret = attr(*args, **kwargs) File "/usr/local/lib/python3.4/dist-packages/KleverCore-0.1rc2.dev367_ng322669b-py3.4.egg/core/vtg/abkm/__init__.py", line 31, in generate_verification_tasks self.decide_verification_task() File "/usr/local/lib/python3.4/dist-packages/KleverCore-0.1rc2.dev367_ng322669b-py3.4.egg/core/utils.py", line 38, in callbacks_caller ret = attr(*args, **kwargs) File "/usr/local/lib/python3.4/dist-packages/KleverCore-0.1rc2.dev367_ng322669b-py3.4.egg/core/vtg/abkm/__init__.py", line 227, in decide_verification_task dom = minidom.parse(fp) File "/usr/lib/python3.4/xml/dom/minidom.py", line 1960, in parse return expatbuilder.parse(file) File "/usr/lib/python3.4/xml/dom/expatbuilder.py", line 913, in parse result = builder.parseFile(file) File "/usr/lib/python3.4/xml/dom/expatbuilder.py", line 211, in parseFile parser.Parse("", True) xml.parsers.expat.ExpatError: no element found: line 1, column 0 2016-06-04 14:23:50 (utils.py:467) ABKM DEBUG> Create unknown report ... </pre> It turns out that generally CPAchecker was terminated due to the time limit was reached but this happens when it still wasn't implemented well - see description of outputs the original issue error trace and the related discussion below. witness. So these files exist but weren't completed. At our side they are parsed with the exception above. This parsing is performed to deal with so called incomplete unsafes, i.e. when a verification status is unknown, but there is one or more error traces. Something should be done with that. For instance, these files can be deleted after CPAchecker was terminated if it will be detected that they weren't completed. For the latter reading the CPAchecker log file can be likely required. As I understand soft time limits will not always help since dumping error traces or/and other output files can take unpredictably much time.