Skip to content

Commit 8397046

Browse files
committed
Quit when there are no properties to verify
We give a "vacuous" successful message
1 parent 1203571 commit 8397046

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

backends.py

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -163,6 +163,9 @@ def simulate(self, fname, info, simulate):
163163
def verify(self, fname, info):
164164
"""Verifies the correctness of the program at fname.
165165
"""
166+
if self.kwargs.get("no_properties") or not info.properties:
167+
log.info("No property to verify!")
168+
return ExitStatus.SUCCESS
166169
args = self.debug_args if self.kwargs["debug"] else self.args
167170
cmd = [self.command, *self.filename_argument(fname), *args]
168171
if self.kwargs.get("timeout", 0) > 0:
@@ -321,6 +324,9 @@ def check_cadp(self):
321324
def verify(self, fname, info):
322325
if not(self.check_cadp()):
323326
return ExitStatus.BACKEND_ERROR
327+
if self.kwargs.get("no_properties") or not info.properties:
328+
log.info("No property to verify!")
329+
return ExitStatus.SUCCESS
324330
modality = info.properties[0].split()[0]
325331
mcl = "fairly.mcl" if modality == "finally" else "never.mcl"
326332
mcl = str(Path("cadp") / Path(mcl))
@@ -405,6 +411,9 @@ def _mcl_fname(self, fname):
405411
def verify(self, fname, info):
406412
if not(self.check_cadp()):
407413
return ExitStatus.BACKEND_ERROR
414+
if self.kwargs.get("no_properties") or not info.properties:
415+
log.info("No property to verify!")
416+
return ExitStatus.SUCCESS
408417
mcl = translate_property(info)
409418
mcl_fname = self._mcl_fname(fname)
410419
log.debug(f"Writing MCL query to {mcl_fname}...")

0 commit comments

Comments
 (0)