/
gnatprove.gpr
87 lines (67 loc) · 2.5 KB
/
gnatprove.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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
with "gnatcoll";
with "gpr2";
project GNATprove is
for Object_Dir use "obj";
for Exec_Dir use "install/bin";
for Languages use ("Ada", "C");
type Build_Type is ("Debug", "Production", "Coverage");
Build : Build_Type := External ("Build", "Debug");
Target := project'Target;
Sources := (".", "src/gnatprove", "src/common");
Sources := Sources & ("src/common/" & Target);
for Source_Dirs use Sources;
for Main use ("gnatprove.adb",
"spark_report.adb",
"spark_memcached_wrapper.adb",
"spark_semaphore_wrapper.adb");
Common_Switches := ("-gnatyg", "-g", "-gnat2022");
package Builder is
for Executable ("gnatprove.adb") use "gnatprove";
for Executable ("spark_report.adb") use "spark_report";
for Executable ("spark_memcached_wrapper.adb") use "spark_memcached_wrapper";
for Executable ("spark_semaphore_wrapper.adb") use "spark_semaphore_wrapper";
case Build is
when "Debug" =>
for Global_Configuration_Pragmas use "gnatprove.adc";
when "Production" =>
null;
when "Coverage" =>
-- We don't do coverage of gnatprove yet, only gnat2why
null;
end case;
end Builder;
package Compiler is
case Build is
when "Debug" =>
for Default_Switches ("Ada") use
Common_Switches & ("-O0", "-gnata", "-gnatwae", "-gnatVa");
when "Production" =>
for Default_Switches ("Ada") use
Common_Switches & ("-O2", "-gnatn");
when "Coverage" =>
-- We don't do coverage of gnatprove yet, only gnat2why
null;
end case;
end Compiler;
package Linker is
case Target is
when "x86-linux" | "x86_64-linux" =>
for Default_Switches ("Ada") use ("-pthread");
when others =>
null;
end case;
end Linker;
package Analyzer is
-- Exclude source files leading to false positives
for Excluded_Source_Files use
("assumptions.ads",
"assumptions.adb",
"print_table.adb",
"configuration.adb",
"report_database.ads"); -- spurious codepeer violation U804-011
for Switches ("analyze") use ("-j0", "--no-gnatcheck");
for Switches ("infer") use ("--disable-issue-type", "MEMORY_LEAK_ADA");
for Switches ("inspector") use ("--legacy-level", "1", "-gnatws");
for Review_File use "gnatprove.sar";
end Analyzer;
end GNATprove;