ada/code_examples_server
0
0
Fork 0
mirror of https://github.com/AdaCore/code_examples_server.git synced 2026-02-12 12:45:18 -08:00
Code Issues Packages Projects Releases Wiki Activity

fixup spark main template

Browse Source
This commit is contained in:
Nicolas Setton
2018-06-01 21:54:23 -04:00
parent 41d10cff79
commit 0905cd2dc7
8 changed files with 75 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
resources/templates/spark_main/example.yaml
View File

@@ -1,3 +1,2 @@
name: SPARK Main
description: Simple overrideable provable main
main: main

1
resources/templates/spark_main/gnatprove/abdasd.adb.stderr Normal file
View File

@@ -0,0 +1 @@
abdasd.adb:1:01: compilation unit expected

0
resources/templates/spark_main/gnatprove/abdasd.adb.stdout Normal file
View File

1
resources/templates/spark_main/gnatprove/gnatprove.out Normal file
View File

@@ -0,0 +1 @@

71
resources/templates/spark_main/gnatprove/why3.conf Normal file
View File

@@ -0,0 +1,71 @@
[main]
magic = 14
memlimit = 0
[editor coqide]
name = "CoqIDE"
command = "coqide -I %l/coq-tactic -R %o/why3_libs/coq Why3 %f"
[prover]
command = "alt-ergo -max-split 5 %f"
command_steps = "alt-ergo -steps-bound %S -max-split 5 %f"
driver = "alt-ergo_gnatprove.drv"
name = "altergo"
shortcut = "altergo"
version = "1.30-gnatprove"
[prover]
command = "cvc4 --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
command_steps = "cvc4 --rlimit=%S --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
driver = "cvc4_gnatprove.drv"
name = "CVC4"
shortcut = "cvc4"
version = "1.6-gnatprove"
[prover]
command = "cvc4 --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
command_steps = "cvc4 --rlimit=%S --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
driver = "cvc4_gnatprove_extra_axioms.drv"
name = "CVC4_More_Axioms"
shortcut = "cvc4_axioms"
version = "1.6-gnatprove"
[prover]
command = "cvc4 --lang=smt2 --stats --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
command_steps = "cvc4 --rlimit=%S --lang=smt2 --stats --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
driver = "cvc4_gnatprove_qf.drv"
name = "CVC4_QF"
shortcut = "cvc4_qf"
version = "1.6-gnatprove"
[prover]
command = "cvc4 --tlimit-per=%t000 --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 --macros-quant --quiet %f"
command_steps = "cvc4 --rlimit=%S --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 --macros-quant --quiet %f"
driver = "cvc4_gnatprove_ce.drv"
name = "CVC4_CE"
shortcut = "cvc4_ce"
version = "1.6-gnatprove"
[prover]
command = "z3 -smt2 -st %f"
command_steps = "z3 rlimit=%S -smt2 -st %f"
driver = "z3_gnatprove.drv"
name = "Z3"
shortcut = "z3"
version = "4.5.1-gnatprove"
[prover]
command = "z3 -smt2 -st %f"
command_steps = "z3 rlimit=%S -smt2 -st %f"
driver = "z3_no_quant.drv"
name = "Z3_noquant"
shortcut = "z3_noquant"
version = "4.5.1-gnatprove"
[prover]
command = "z3 -t:%t -smt2 -st %f"
command_steps = "z3 rlimit=%S -smt2 -st %f"
driver = "z3_gnatprove_ce.drv"
name = "z3_ce"
shortcut = "z3_ce"
version = "4.5.1-gnatprove"
[prover]
command = "coqtop -batch -I %l/coq-tactic -R %o/why3_libs/coq Why3 -l %f"
driver = "coq_gnatprove.drv"
name = "Coq"
shortcut = "coq"
version = "8.5pl2"
interactive = true
editor = "coqide"
in_place = false

4
resources/templates/spark_main/main.adb
View File

@@ -1,4 +0,0 @@
procedure Main is
begin
null;
end Main;

1
resources/templates/spark_main/main.adc
View File

@@ -4,3 +4,4 @@ pragma Partition_Elaboration_Policy(Sequential);
pragma SPARK_Mode (On);
pragma Warnings (Off, "no Global contract available");
pragma Warnings (Off, "subprogram * has no effect");
pragma Warnings (Off, "file name does not match");

4
resources/templates/spark_main/main.gpr
View File

@@ -1,9 +1,7 @@
project Main is
for Main use ("main.adb");
package Compiler is
for Switches ("ada") use ("-g", "-gnatwa", "-gnatQ");
for Switches ("ada") use ("-g");
end Compiler;
package Builder is