forked from AdaCore/Platinum_Reusable_Stack
-
Notifications
You must be signed in to change notification settings - Fork 0
/
stack_dev.gpr
72 lines (56 loc) · 1.98 KB
/
stack_dev.gpr
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
project Stack_Dev is
for Languages use ("Ada");
for Exec_Dir use ".";
package Compiler is
for Default_Switches ("ada") use
("-gnatwa", -- enable additional warnings
"-g", -- enable debugging info, in case
"-gnato11", -- enable overflow checks everywhere, which is also the default
"-gnata"); -- enable assertions
end Compiler;
package Builder is
for Switches ("ada") use ("-g");
end Builder;
type Adoption_Levels is ("Ada", "Stone", "Bronze", "Silver", "Gold", "Platinum");
Adoption_Level : Adoption_Levels := external ("Adoption_Level", "Platinum");
for Object_Dir use "objs/" & Adoption_Level;
-- set main program
case Adoption_Level is
when "Ada" | "Stone" | "Bronze" | "Silver" =>
for Main use ("demo_aorte.adb");
when "Gold" | "Platinum" =>
for Main use ("demo_gold.adb");
end case;
-- set source dirs
case Adoption_Level is
when "Ada" =>
for Source_Dirs use ("source/mains", "source/Ada");
when "Stone" =>
for Source_Dirs use ("source/mains", "source/Stone");
when "Bronze" =>
for Source_Dirs use ("source/mains", "source/Bronze");
when "Silver" =>
for Source_Dirs use ("source/mains", "source/Silver");
when "Gold" =>
for Source_Dirs use ("source/mains", "source/Gold");
when "Platinum" =>
for Source_Dirs use ("source/mains", "source/Platinum");
end case;
-- set GNATprove mode switch
Mode_Switch := "";
case Adoption_Level is
when "Ada" =>
Mode_Switch := "--mode=check";
when "Stone" =>
Mode_Switch := "--mode=check_all";
when "Bronze" =>
Mode_Switch := "--mode=bronze";
when "Silver" | "Gold" | "Platinum" =>
Mode_Switch := "--mode=all";
end case;
-- set prover switches
package Prove is
for Proof_Switches ("Ada") use
("--level=4") & Mode_Switch;
end Prove;
end Stack_Dev;