@@ -113,21 +113,21 @@ def cleanup_project(language, project_filename, main_file):
113113 #
114114 # Clean-up source-code examples after compilation
115115 #
116- if project_filename is not None :
116+ if language == "ada" :
117+ if project_filename is not None :
117118
118- try :
119- run ("gprclean" , "-P" , project_filename )
120- except S .CalledProcessError as e :
121- out = str (e .output .decode ("utf-8" ))
122- print_error (loc , "Failed to clean-up example" )
123- print (out )
124-
125- try :
126- run ("gnatprove" , "-P" , project_filename , "--clean" )
127- except S .CalledProcessError as e :
128- out = str (e .output .decode ("utf-8" ))
119+ try :
120+ run ("gprclean" , "-P" , project_filename )
121+ except S .CalledProcessError as e :
122+ out = str (e .output .decode ("utf-8" ))
123+ print_error (loc , "Failed to clean-up example" )
124+ print (out )
129125
130- if language == "c" :
126+ try :
127+ run ("gnatprove" , "-P" , project_filename , "--clean" )
128+ except S .CalledProcessError as e :
129+ out = str (e .output .decode ("utf-8" ))
130+ elif language == "c" :
131131 try :
132132 cmd = ["rm" , "-f" ] + glob .glob ('*.o' ) + glob .glob ('*.gch' )
133133 if main_file is not None :
@@ -421,17 +421,14 @@ def cleanup_project(language, project_filename, main_file):
421421 or 'ada-report-all' in block .classes :
422422 extra_args = ["--report=all" ]
423423
424- line = None
425- if block .gnatprove_version [1 ].startswith ("14" ):
426- line = ["gnatprove" , "-P" , block .spark_project_filename ,
427- "--checks-as-errors=on" , "--level=0" ,
428- "--function-sandboxing=off" , "--output=oneline" ]
429- elif block .gnatprove_version [1 ].startswith ("12" ):
424+ # Default switches for GNATprove 14 and above
425+ line = ["gnatprove" , "-P" , block .spark_project_filename ,
426+ "--checks-as-errors=on" , "--level=0" ,
427+ "--function-sandboxing=off" , "--output=oneline" ]
428+ if block .gnatprove_version [1 ].startswith ("12" ):
430429 line = ["gnatprove" , "-P" , block .spark_project_filename ,
431430 "--checks-as-errors" , "--level=0" ,
432431 "--no-axiom-guard" , "--output=oneline" ]
433- else :
434- prove_error = True
435432
436433 line .extend (extra_args )
437434
0 commit comments