Skip to content

Commit b3bcdc0

Browse files
committed
Revert " backends.py: add simulation to CBMC backend"
This reverts commit 6df61b2.
1 parent 887032f commit b3bcdc0

File tree

1 file changed

+0
-26
lines changed

1 file changed

+0
-26
lines changed

backends.py

Lines changed: 0 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -294,32 +294,6 @@ def get_cmdline(self, fname, _):
294294
cmd.append(fname)
295295
return cmd
296296

297-
def simulate(self, fname, info):
298-
exe = os.environ.get("CBMC") or (
299-
str(self.cwd / "backends" / "cbmc-5.42.0" / "bin" / "cbmc")
300-
if "Linux" in platform.system()
301-
else "cbmc")
302-
glucose = str(self.cwd / "backends" / "glucose" / "glucose-nondet.sh")
303-
cmd = [
304-
exe,
305-
"--external-sat-solver", glucose,
306-
"--trace",
307-
"--stop-on-fail"
308-
]
309-
cmd.append(fname)
310-
log_call(cmd)
311-
try:
312-
out = check_output(cmd, stderr=STDOUT, cwd=self.cwd).decode()
313-
self.verbose_output(out, "Backend output")
314-
except CalledProcessError as err:
315-
out = err.output.decode("utf-8")
316-
self.verbose_output(out, "Backend output")
317-
try:
318-
print(*translateCPROVER(out, fname, info), sep="", end="")
319-
except Exception as e:
320-
print(f"Counterexample translation failed: {e}")
321-
return ExitStatus.SUCCESS
322-
323297
def check_cli(self):
324298
super().check_cli()
325299
if not self.cli[Args.STEPS] and not self.cli[Args.SHOW]:

0 commit comments

Comments
 (0)