From bc28bc1da6a88bfddf2603812658871f126583c0 Mon Sep 17 00:00:00 2001 From: gusthoff Date: Sun, 8 Jun 2025 12:34:18 +0200 Subject: [PATCH 1/3] Test script: only run block in case of language set to Ada Only run GPRclean/GNATprove for Ada blocks, avoid running them for C. --- .../code_projects/check_code_block.py | 26 +++++++++---------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/frontend/py_modules/code_projects/check_code_block.py b/frontend/py_modules/code_projects/check_code_block.py index bb513d16d..580e1cb2f 100755 --- a/frontend/py_modules/code_projects/check_code_block.py +++ b/frontend/py_modules/code_projects/check_code_block.py @@ -113,21 +113,21 @@ def cleanup_project(language, project_filename, main_file): # # Clean-up source-code examples after compilation # - if project_filename is not None: + if language == "ada": + if project_filename is not None: - try: - run("gprclean", "-P", project_filename) - except S.CalledProcessError as e: - out = str(e.output.decode("utf-8")) - print_error(loc, "Failed to clean-up example") - print(out) - - try: - run("gnatprove", "-P", project_filename, "--clean") - except S.CalledProcessError as e: - out = str(e.output.decode("utf-8")) + try: + run("gprclean", "-P", project_filename) + except S.CalledProcessError as e: + out = str(e.output.decode("utf-8")) + print_error(loc, "Failed to clean-up example") + print(out) - if language == "c": + try: + run("gnatprove", "-P", project_filename, "--clean") + except S.CalledProcessError as e: + out = str(e.output.decode("utf-8")) + elif language == "c": try: cmd = ["rm", "-f"] + glob.glob('*.o') + glob.glob('*.gch') if main_file is not None: From fb2079c594be0b058246d6e6b451c1f30fcf995f Mon Sep 17 00:00:00 2001 From: gusthoff Date: Sun, 8 Jun 2025 12:37:43 +0200 Subject: [PATCH 2/3] Test script: use GNATprove 14+ command-line switches as the default --- .../py_modules/code_projects/check_code_block.py | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/frontend/py_modules/code_projects/check_code_block.py b/frontend/py_modules/code_projects/check_code_block.py index 580e1cb2f..5bc8e6332 100755 --- a/frontend/py_modules/code_projects/check_code_block.py +++ b/frontend/py_modules/code_projects/check_code_block.py @@ -421,17 +421,14 @@ def cleanup_project(language, project_filename, main_file): or 'ada-report-all' in block.classes: extra_args = ["--report=all"] - line = None - if block.gnatprove_version[1].startswith("14"): - line = ["gnatprove", "-P", block.spark_project_filename, - "--checks-as-errors=on", "--level=0", - "--function-sandboxing=off", "--output=oneline"] - elif block.gnatprove_version[1].startswith("12"): + # Default switches for GNATprove 14 and above + line = ["gnatprove", "-P", block.spark_project_filename, + "--checks-as-errors=on", "--level=0", + "--function-sandboxing=off", "--output=oneline"] + if block.gnatprove_version[1].startswith("12"): line = ["gnatprove", "-P", block.spark_project_filename, "--checks-as-errors", "--level=0", "--no-axiom-guard", "--output=oneline"] - else: - prove_error = True line.extend(extra_args) From afd7e8916fa2fc744acdf3cfcb0d7ed63b381fed Mon Sep 17 00:00:00 2001 From: gusthoff Date: Sun, 8 Jun 2025 12:39:08 +0200 Subject: [PATCH 3/3] Test script: fix setting main file for SPARK project Do not set the filename in case of no main file. --- frontend/py_modules/code_projects/extract_projects.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/frontend/py_modules/code_projects/extract_projects.py b/frontend/py_modules/code_projects/extract_projects.py index cdd5ddfe0..c12d4ff68 100755 --- a/frontend/py_modules/code_projects/extract_projects.py +++ b/frontend/py_modules/code_projects/extract_projects.py @@ -365,7 +365,8 @@ def get_main_filename(block): if block.language == "ada": - block.project_main_file = get_main_filename(block) + if block.run_it: + block.project_main_file = get_main_filename(block) block.spark_project_filename = write_project_file(block.project_main_file, block.compiler_switches, spark_mode=True)