From 326d1cce1631913fbe64216c4e2661a52e0d92f0 Mon Sep 17 00:00:00 2001 From: dreast Date: Fri, 29 May 2026 10:09:24 -0400 Subject: [PATCH] Applied MemlimitProof tests directory changes onto daidalus_integration from afrl-rq --- tests/proof/proofs/route_aggregator/test.yaml | 3 ++- tests/proof/run-proofs.py | 11 +++++++++++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/tests/proof/proofs/route_aggregator/test.yaml b/tests/proof/proofs/route_aggregator/test.yaml index d6f9fcc58..167847b21 100644 --- a/tests/proof/proofs/route_aggregator/test.yaml +++ b/tests/proof/proofs/route_aggregator/test.yaml @@ -1,3 +1,4 @@ filenames: ["route_aggregator.ads"] level: 4 -timeout: 120 \ No newline at end of file +timeout: 120 +memlimit: 4000 \ No newline at end of file diff --git a/tests/proof/run-proofs.py b/tests/proof/run-proofs.py index c5e5f6e4f..4cbd70382 100644 --- a/tests/proof/run-proofs.py +++ b/tests/proof/run-proofs.py @@ -15,6 +15,7 @@ def run(self): filenames = self.test_env.get ("filenames") gnatprove_level = self.test_env.get ("level") gnatprove_timeout = self.test_env.get ("timeout") + gnatprove_memlimit= self.test_env.get("memlimit") if filenames != None: if self.env.options.no_replay: @@ -29,6 +30,8 @@ def run(self): proof_switches+= ["--level="+str(gnatprove_level)] if gnatprove_timeout != None: proof_switches+=["--timeout="+str(gnatprove_timeout)] + if gnatprove_memlimit != None: + proof_switches +=["--memlimit="+str(gnatprove_memlimit)] else: proof_switches=["--replay"] @@ -61,6 +64,14 @@ def add_options(self, ArgumentParser): default=300, help="Modify the timeout of processes running gnatprove (not related to gnatprove's --timeout option)" ) + self.main.argument_parser.add_argument( + "--memlimit", + dest="timeout", + type=int, + metavar="N", + default=4000, + help="Modify the memory limit of processes running gnatprove (in MB)" + ) self.main.argument_parser.add_argument( "-g", "--gnatprove-jobs",