Skip to content
This repository was archived by the owner on Aug 12, 2024. It is now read-only.

Commit b48c091

Browse files
committed
employ style checks
fixes #21
1 parent 6b64d8d commit b48c091

File tree

5 files changed

+93
-4
lines changed

5 files changed

+93
-4
lines changed

.travis.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ services:
66
- docker
77

88
script:
9-
- docker run -v $PWD:/basalt -t jklmnn/componolit-ci:latest-gnat /bin/sh -c "gprbuild -P /basalt/test/aunit/test.gpr && /basalt/test/aunit/obj/test && gnatprove -P /basalt/test/proof/proof.gpr --level=2 --report=all --checks-as-errors"
9+
- docker run -v $PWD:/basalt -t jklmnn/componolit-ci:latest-gnat /bin/sh -c "gprbuild -P /basalt/basalt.gpr && gprclean -P /basalt/basalt.gpr && gprbuild -P /basalt/test/aunit/test.gpr -XBUILD=test && /basalt/test/aunit/obj/test && gnatprove -P /basalt/test/proof/proof.gpr --level=2 --report=all --checks-as-errors"
1010

1111
after_script:
1212
- cat test/proof/obj/gnatprove/gnatprove.out

basalt.gpr

+16-3
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,12 @@
11

2+
with "switches.gpr";
3+
24
library project Basalt is
35

46
type Library_Type is ("dynamic", "static");
5-
Kind : Library_Type := external ("KIND", "dynamic");
7+
type Build_Type is ("default", "test");
8+
Kind : Library_Type := external ("KIND", "dynamic");
9+
Build : Build_Type := external ("BUILD", "default");
610

711
for Create_Missing_Dirs use "True";
812
for Source_Dirs use ("src");
@@ -13,12 +17,21 @@ library project Basalt is
1317
for Library_Dir use "lib";
1418
for Library_Kind use Kind;
1519

20+
package Builder is
21+
case Build is
22+
when "default" =>
23+
for Global_Configuration_Pragmas use "restrictions.adc";
24+
when "test" =>
25+
for Global_Configuration_Pragmas use "test_restrictions.adc";
26+
end case;
27+
end Builder;
28+
1629
package Compiler is
1730
case Kind is
1831
when "dynamic" =>
19-
null;
32+
for Default_Switches ("Ada") use Switches.Compiler_Switches;
2033
when "static" =>
21-
for Default_Switches ("Ada") use ("-fPIC");
34+
for Default_Switches ("Ada") use ("-fPIC") & Switches.Compiler_Switches;
2235
end case;
2336
end Compiler;
2437

restrictions.adc

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
pragma Restrictions (No_Allocators);
2+
pragma Restrictions (No_Calendar);
3+
pragma Restrictions (No_Enumeration_Maps);
4+
pragma Restrictions (No_Exceptions);
5+
pragma Restrictions (No_Exception_Handlers);
6+
pragma Restrictions (No_Implicit_Dynamic_Code);
7+
pragma Restrictions (No_Initialize_Scalars);
8+
pragma Restrictions (No_IO);
9+
pragma Restrictions (No_Streams);
10+
pragma Restrictions (No_Tasking);
11+
pragma Restrictions (Static_Storage_Size);
12+
pragma SPARK_Mode (On);

switches.gpr

+64
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
abstract project Switches
2+
is
3+
Compiler_Switches :=
4+
(
5+
"-gnatA" -- Avoid processing gnat.adc, if present file will be ignored
6+
7+
-- ,"-gnatef" -- Full source path in brief error messages
8+
9+
-- Disabled due to a bug in GNAT Community 2018
10+
--,"-gnateV" -- Validity checks on subprogram parameters
11+
12+
,"-gnatf" -- Full errors. Verbose details, all undefined references
13+
,"-gnatU" -- Enable unique tag for error messages
14+
15+
-- Validity checks
16+
,"-gnatVa" -- turn on all validity checking options
17+
18+
-- Warnings
19+
,"-gnatwa" -- turn on all info/warnings marked with + in gnatmake help
20+
,"-gnatwe" -- treat all warnings (but not info) as errors
21+
,"-gnatwd" -- turn on warnings for implicit dereference
22+
,"-gnatwh" -- turn on warnings for hiding declarations
23+
,"-gnatwk" -- turn on warnings for standard redefinition
24+
,"-gnatwt" -- turn on warnings for tracking deleted code
25+
,"-gnatwu" -- turn on warnings for unordered enumeration
26+
27+
-- Style checks
28+
,"-gnaty3" -- Check indentation (3 spaces)
29+
,"-gnatya" -- check attribute casing
30+
,"-gnatyA" -- check array attribute indexes
31+
,"-gnatyb" -- check no blanks at end of lines
32+
,"-gnatyc" -- check comment format (two spaces)
33+
,"-gnatyd" -- check no DOS line terminators
34+
,"-gnatye" -- check end/exit labels present
35+
,"-gnatyf" -- check no form feeds/vertical tabs in source
36+
,"-gnatyh" -- check no horizontal tabs in source
37+
,"-gnatyi" -- check if-then layout
38+
,"-gnatyI" -- check mode in
39+
,"-gnatyk" -- check casing rules for keywords
40+
,"-gnatyl" -- check reference manual layout
41+
,"-gnatyL8" -- check max nest level < nn
42+
,"-gnatyM120" -- check line length <= nn characters
43+
,"-gnatyn" -- check casing of package Standard identifiers
44+
,"-gnatyO" -- check overriding indicators
45+
,"-gnatyp" -- check pragma casing
46+
,"-gnatyr" -- check casing for identifier references
47+
,"-gnatys" -- check separate subprogram specs present
48+
,"-gnatyS" -- check separate lines after THEN or ELSE
49+
,"-gnatyt" -- check token separation rules
50+
,"-gnatyu" -- check no unnecessary blank lines
51+
,"-gnatyx" -- check extra parentheses around conditionals
52+
53+
);
54+
55+
Compiler_Debug_Switches :=
56+
(
57+
"-fstack-check" -- dynamic stack checking
58+
,"-gnata" -- Enable pragma Assert/Debug
59+
,"-gnato" -- Overflow checking
60+
,"-g" -- Debug symbols
61+
,"-O0" -- Debug symbols
62+
);
63+
64+
end Switches;

test_restrictions.adc

Whitespace-only changes.

0 commit comments

Comments
 (0)