Skip to content

Commit f7c4412

Browse files
committed
testing: HOL-Light: add support for cross-proofing
This commit introduces a new flag --arch to the hol_light command of the tests script that allows user specification of which architecture to run/list the proofs for. If not passed, the behavior is unchanged. Signed-off-by: Andreas Hatziiliou <andreas.hatziiliou@savoirfairelinux.com>
1 parent 183f280 commit f7c4412

1 file changed

Lines changed: 11 additions & 1 deletion

File tree

scripts/tests

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1015,7 +1015,9 @@ class Tests:
10151015
self.check_fail()
10161016

10171017
def hol_light(self):
1018-
if platform.machine().lower() in ["arm64", "aarch64"]:
1018+
if self.args.arch:
1019+
arch = self.args.arch
1020+
elif platform.machine().lower() in ["arm64", "aarch64"]:
10191021
arch = "aarch64"
10201022
elif platform.machine().lower() in ["x86_64"]:
10211023
arch = "x86_64"
@@ -1479,6 +1481,14 @@ def cli():
14791481
default=False,
14801482
)
14811483

1484+
hol_light_parser.add_argument(
1485+
"-a",
1486+
"--arch",
1487+
help="Architecture for which to list/run HOL_LIGHT proofs (aarch64 or x86_64).",
1488+
choices=["aarch64", "x86_64"],
1489+
default=None,
1490+
)
1491+
14821492
# func arguments
14831493
func_parser = cmd_subparsers.add_parser(
14841494
"func",

0 commit comments

Comments
 (0)