45 lines
1.4 KiB
Python
45 lines
1.4 KiB
Python
import os
|
|
|
|
import infra.basetest
|
|
|
|
|
|
class TestZ3(infra.basetest.BRTest):
|
|
# Need to use a different toolchain than the default due to
|
|
# z3 requiring fenv.h not provided by uclibc.
|
|
config = \
|
|
"""
|
|
BR2_arm=y
|
|
BR2_TOOLCHAIN_EXTERNAL=y
|
|
BR2_TOOLCHAIN_EXTERNAL_BOOTLIN=y
|
|
BR2_TOOLCHAIN_EXTERNAL_BOOTLIN_ARMV5_EABI_GLIBC_STABLE=y
|
|
BR2_PACKAGE_PYTHON3=y
|
|
BR2_PACKAGE_Z3=y
|
|
BR2_PACKAGE_Z3_PYTHON=y
|
|
BR2_ROOTFS_OVERLAY="{}"
|
|
BR2_TARGET_ROOTFS_CPIO=y
|
|
# BR2_TARGET_ROOTFS_TAR is not set
|
|
""".format(
|
|
# overlay to add a z3 smt and python test scripts
|
|
infra.filepath("tests/package/test_z3/rootfs-overlay"))
|
|
|
|
def test_run(self):
|
|
cpio_file = os.path.join(self.builddir, "images", "rootfs.cpio")
|
|
self.emulator.boot(arch="armv5",
|
|
kernel="builtin",
|
|
options=["-initrd", cpio_file])
|
|
self.emulator.login()
|
|
|
|
# Check program executes
|
|
cmd = "z3 --version"
|
|
self.assertRunOk(cmd)
|
|
|
|
# Run a basic smt2 example
|
|
cmd = "z3 /root/z3test.smt2"
|
|
output, exit_code = self.emulator.run(cmd)
|
|
self.assertEqual(exit_code, 0)
|
|
self.assertEqual(output[0], "unsat")
|
|
|
|
# Run a basic python example
|
|
cmd = "/root/z3test.py"
|
|
self.assertRunOk(cmd, timeout=10)
|