diff --git a/compile_server/app/checker.py b/compile_server/app/checker.py index ca3a6dc..6177c7e 100644 --- a/compile_server/app/checker.py +++ b/compile_server/app/checker.py @@ -46,11 +46,6 @@ from compile_server.app.views import CrossDomainResponse gnatprove_found = False -ALLOWED_EXTRA_ARGS = {'spark-flow': "--mode=flow", - 'spark-report-all': "--report=all"} -# We maintain a list of extra arguments that can be passed to the command -# line. For security we don't want the user to pass arguments as-is. - PROCESSES_LIMIT = 300 # The limit of processes that can be running RECEIVED_FILE_CHAR_LIMIT = 50 * 1000 @@ -173,14 +168,6 @@ def check_program(request): command = ["gnatprove", "-P", "main", "--checks-as-errors", "--level=0", "--no-axiom-guard"] - # Process extra_args - if 'extra_args' in received_json: - extra_args = received_json['extra_args'] - if extra_args: - if extra_args not in ALLOWED_EXTRA_ARGS: - return CrossDomainResponse( - {'identifier': '', 'message': "extra_args not known"}) - command.append(ALLOWED_EXTRA_ARGS[extra_args]) print " ".join(command) try: p = process_handling.SeparateProcess([command], tempd) diff --git a/infrastructure/container_payload/run.py b/infrastructure/container_payload/run.py index 104381a..5ccf571 100644 --- a/infrastructure/container_payload/run.py +++ b/infrastructure/container_payload/run.py @@ -118,8 +118,9 @@ def safe_run(workdir, mode): c(["echo"]) try: + main = extract_main(workdir) + if mode == "run": - main = extract_main(workdir) doctor_main_gpr(workdir, main, False) # In "run" mode, first build, and then launch the main @@ -135,11 +136,22 @@ def safe_run(workdir, mode): c(line) elif mode == "prove": - main = extract_main(workdir) doctor_main_gpr(workdir, main, spark_mode=True) line = ["gnatprove", "-P", "main", "--checks-as-errors", "--level=0", "--no-axiom-guard"] c(line) + elif mode == "prove_flow": + doctor_main_gpr(workdir, main, spark_mode=True) + line = ["gnatprove", "-P", "main", "--checks-as-errors", + "--level=0", "--no-axiom-guard", "--mode=flow"] + c(line) + + elif mode == "prove_report_all": + doctor_main_gpr(workdir, main, spark_mode=True) + line = ["gnatprove", "-P", "main", "--checks-as-errors", + "--level=0", "--no-axiom-guard", "--report=all"] + c(line) + else: print "mode not implemented" @@ -149,7 +161,8 @@ def safe_run(workdir, mode): finally: if os.path.isdir(workdir): time.sleep(0.2) # Time for the filesystem to sync - c(["rm", "-rf", workdir]) + if not DEBUG: + c(["rm", "-rf", workdir]) if __name__ == '__main__':