Skip to content

Commit

Permalink
Merge branch 'topic/739-dross-update-proof-of-light-runtime' into 'ma…
Browse files Browse the repository at this point in the history
…ster'

Increase level for SPARK proofs of the runtime

See merge request eng/toolchain/bb-runtimes!136
  • Loading branch information
clairedross committed Nov 4, 2024
2 parents c69c59a + dd8869e commit 15d4fd0
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion support/data/runtime_build.gpr.in
Original file line number Diff line number Diff line change
Expand Up @@ -64,12 +64,13 @@ project Runtime_Build is
for Proof_Switches ("Ada") use ("-j0", "--level=2", "--function-sandboxing=off", "--counterexamples=off");

-- Specialize the command-line for more complex units (-j0 is implied)
for Proof_Switches ("a-strmap.adb") use ("--level=3");
for Proof_Switches ("a-strfix.adb") use ("--level=4");
for Proof_Switches ("a-strsea.adb") use ("--level=4");
for Proof_Switches ("a-strsup.adb") use ("--level=4", "--timeout=30");
for Proof_Switches ("i-c.adb") use ("--level=4", "--timeout=120");
for Proof_Switches ("s-arit32.adb") use ("--level=3", "--prover=all");
for Proof_Switches ("s-arit64.adb") use ("--level=3", "--prover=all");
for Proof_Switches ("s-arit64.adb") use ("--level=4", "--prover=all");
for Proof_Switches ("s-expmod.adb") use ("--level=2");
for Proof_Switches ("s-imgboo.adb") use ("--level=3");
for Proof_Switches ("s-valboo.adb") use ("--level=3");
Expand Down

0 comments on commit 15d4fd0

Please sign in to comment.