Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 18 additions & 21 deletions frontend/py_modules/code_projects/check_code_block.py
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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)

Expand Down
3 changes: 2 additions & 1 deletion frontend/py_modules/code_projects/extract_projects.py
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
Loading