Skip to content
This repository was archived by the owner on May 22, 2023. It is now read-only.

Commit 355ee1e

Browse files
jklmnnjklmnn
committedJun 2, 2020
Compile and prove with GNAT CE 2020 and 2019
ref #178
·
v0.2.0
1 parent 86dd3aa commit 355ee1e

27 files changed

+293
-32
lines changed
 

‎cement

+9-3
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,9 @@ prove_parser.add_argument("-u", "--unit", help="ada unit")
3131
prove_parser.add_argument("-s", "--steps", help="prove steps", default="8000")
3232
prove_parser.add_argument("paths", help="component search paths", nargs="*")
3333

34+
def get_gcc_version():
35+
return subprocess.check_output(["gcc", "-dumpversion"]).decode('utf-8').strip().split('.')[0]
36+
3437
def get_component_name(libname):
3538
return libname[13:-3]
3639

@@ -96,7 +99,8 @@ def gpr_compile(config, gneiss_root, build_dir, root_dir, paths, platform, logge
9699
logger.info("Compiling...")
97100
components = get_component_files(config)
98101
logger.info("Preparing init...")
99-
default_args = ["-p", "-XCEMENT_BUILD_STEP=prepare", "--db", os.path.join(gneiss_root, "gprconfig_db")]
102+
default_args = ["-p", "-XCEMENT_BUILD_STEP=prepare", "--db", os.path.join(gneiss_root, "gprconfig_db"),
103+
"-XGCC_VERSION=" + get_gcc_version()]
100104
if args.verbose:
101105
default_args.append("-v")
102106
if build_init(gneiss_root, build_dir, default_args, platform, logger) > 0:
@@ -113,7 +117,8 @@ def gpr_compile(config, gneiss_root, build_dir, root_dir, paths, platform, logge
113117
logger.error("Preparation of " + c + " failed")
114118
exit(1)
115119
logger.info("Compiling init...")
116-
default_args = ["-p", "-XCEMENT_BUILD_STEP=compile"]
120+
default_args = ["-p", "-XCEMENT_BUILD_STEP=compile",
121+
"-XGCC_VERSION=" + get_gcc_version()]
117122
if verbose:
118123
default_args.append("-v")
119124
if build_init(gneiss_root, build_dir, default_args, platform, logger) > 0:
@@ -157,7 +162,8 @@ def gpr_prepare(name, root, build_dir, paths):
157162
"-XCEMENT_OBJECT_DIR=" + os.path.join(build_dir, name[:-4] + "_obj"),
158163
"-XCEMENT_LIB_OBJECT_DIR=" + os.path.join(build_dir, name[:-4] + "_libobj"),
159164
"-XCEMENT_LIBRARY_DIR=" + os.path.join(build_dir, name[:-4] + "_lib"),
160-
"-XCEMENT_COMPONENT_DIR=" + os.path.join(build_dir, name[:-4] + "_component")]
165+
"-XCEMENT_COMPONENT_DIR=" + os.path.join(build_dir, name[:-4] + "_component"),
166+
"-XGCC_VERSION=" + get_gcc_version()]
161167
project_path_file = "/tmp/cement_gpr_project_path." + str(os.getpid())
162168
with open(project_path_file, "w+") as ppf:
163169
for path in [root] + paths:

‎gneiss_component.gpr

+1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ abstract project Gneiss_Component is
77
Gneiss_Runtime := Gneiss_Root & "/ada-runtime/build/posix/obj";
88
Gneiss_Component_Prefix := "component_";
99
Build_Step := external ("CEMENT_BUILD_STEP");
10+
GCC_Version := external ("GCC_VERSION");
1011

1112
for Library_Options use ("-L" & Gneiss_Root & "/ada-runtime/build/posix/obj/adalib",
1213
"-nostdlib",

‎test/hello_world.gpr

+10-1
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,19 @@
11

22
project Hello_World extends "gneiss_component" is
33

4+
Src_Dirs := ("hello_world");
5+
6+
case GCC_Version is
7+
when "9" =>
8+
Src_Dirs := ("hello_world/gnat_ce_2020") & Src_Dirs;
9+
when others =>
10+
null;
11+
end case;
12+
413
case Build_Step is
514
when "compile" =>
615
for Runtime ("Ada") use Gneiss_Runtime;
7-
for Source_Dirs use ("hello_world");
16+
for Source_Dirs use Src_Dirs;
817
for Object_Dir use external ("CEMENT_OBJECT_DIR");
918
for Library_Name use Gneiss_Component_Prefix & "hello_world";
1019
for Library_Kind use "dynamic";

‎test/hello_world/component.ads

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ with Gneiss_Internal;
66
package Component with
77
SPARK_Mode,
88
Abstract_State => (Component_State, Platform_State),
9-
Initializes => (Platform_State, Main.Platform)
9+
Initializes => Platform_State
1010
is
1111

1212
procedure Construct (Capability : Gneiss.Capability) with

‎test/hello_world/gnat_ce_2020/component.ads

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
2+
with Gneiss;
3+
with Gneiss.Component;
4+
with Gneiss_Internal;
5+
6+
package Component with
7+
SPARK_Mode,
8+
Abstract_State => (Component_State, Platform_State),
9+
Initializes => (Platform_State, Main.Platform)
10+
is
11+
12+
procedure Construct (Capability : Gneiss.Capability) with
13+
Global => (In_Out => (Platform_State,
14+
Gneiss_Internal.Platform_State,
15+
Main.Platform),
16+
Output => Component_State);
17+
18+
procedure Destruct with
19+
Global => (In_Out => (Platform_State, Gneiss_Internal.Platform_State));
20+
21+
package Main is new Gneiss.Component (Construct, Destruct);
22+
23+
end Component;

‎test/linux.sh

+8-12
Original file line numberDiff line numberDiff line change
@@ -10,18 +10,14 @@ make -C ada-runtime
1010

1111
set -e
1212

13-
if [ "$(gcc -dumpversion)" = "9.3.1" ]
14-
then
15-
# Only prove with GNAT CE 2020/GNAT Pro 21
16-
./cement prove test/message_client.gpr . lib test -u component
17-
./cement prove test/message_server.gpr . lib test -u component
18-
./cement prove test/hello_world.gpr . lib test -u component
19-
./cement prove test/log_proxy.gpr . lib test -u component
20-
./cement prove test/rom.gpr . lib test -u component
21-
./cement prove test/memory_client.gpr . lib test -u component
22-
./cement prove test/memory_server.gpr . lib test -u component
23-
./cement prove test/timer.gpr . lib test -u component
24-
fi
13+
./cement prove test/message_client.gpr . lib test -u component
14+
./cement prove test/message_server.gpr . lib test -u component
15+
./cement prove test/hello_world.gpr . lib test -u component
16+
./cement prove test/log_proxy.gpr . lib test -u component
17+
./cement prove test/rom.gpr . lib test -u component
18+
./cement prove test/memory_client.gpr . lib test -u component
19+
./cement prove test/memory_server.gpr . lib test -u component
20+
./cement prove test/timer.gpr . lib test -u component
2521

2622
./cement build test/message_client/message_client.xml . lib test
2723
./cement build test/hello_world/hello_world.xml . lib test

‎test/log_proxy.gpr

+10-1
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,19 @@ with "basalt";
33

44
project Log_Proxy extends "gneiss_component" is
55

6+
Src_Dirs := ("log_proxy");
7+
8+
case GCC_Version is
9+
when "9" =>
10+
Src_Dirs := ("log_proxy/gnat_ce_2020") & Src_Dirs;
11+
when others =>
12+
null;
13+
end case;
14+
615
case Build_Step is
716
when "compile" =>
817
for Runtime ("Ada") use Gneiss_Runtime;
9-
for Source_Dirs use ("log_proxy");
18+
for Source_Dirs use Src_Dirs;
1019
for Object_Dir use external ("CEMENT_OBJECT_DIR");
1120
for Library_Name use Gneiss_Component_Prefix & "log_proxy";
1221
for Library_Kind use "dynamic";

‎test/log_proxy/component.ads

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ with Gneiss_Internal;
66
package Component with
77
SPARK_Mode,
88
Abstract_State => (Component_State, Platform_State),
9-
Initializes => (Platform_State, Main.Platform)
9+
Initializes => Platform_State
1010
is
1111

1212
procedure Construct (Cap : Gneiss.Capability) with

‎test/log_proxy/gnat_ce_2020/component.ads

+24
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
2+
with Gneiss;
3+
with Gneiss.Component;
4+
with Gneiss_Internal;
5+
6+
package Component with
7+
SPARK_Mode,
8+
Abstract_State => (Component_State, Platform_State),
9+
Initializes => (Platform_State, Main.Platform)
10+
is
11+
12+
procedure Construct (Cap : Gneiss.Capability) with
13+
Global => (Output => Component_State,
14+
In_Out => (Platform_State,
15+
Main.Platform,
16+
Gneiss_Internal.Platform_State));
17+
18+
procedure Destruct with
19+
Global => (In_Out => (Platform_State,
20+
Gneiss_Internal.Platform_State));
21+
22+
package Main is new Gneiss.Component (Construct, Destruct);
23+
24+
end Component;

‎test/memory_client.gpr

+10-1
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,19 @@
11

22
project Memory_Client extends "gneiss_component" is
33

4+
Src_Dirs := ("memory_client");
5+
6+
case GCC_Version is
7+
when "9" =>
8+
Src_Dirs := ("memory_client/gnat_ce_2020") & Src_Dirs;
9+
when others =>
10+
null;
11+
end case;
12+
413
case Build_Step is
514
when "compile" =>
615
for Runtime ("Ada") use Gneiss_Runtime;
7-
for Source_Dirs use ("memory_client");
16+
for Source_Dirs use Src_Dirs;
817
for Object_Dir use external ("CEMENT_OBJECT_DIR");
918
for Library_Name use Gneiss_Component_Prefix & "memory_client";
1019
for Library_Kind use "dynamic";

‎test/memory_client/component.ads

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ with Gneiss.Component;
66
package Component with
77
SPARK_Mode,
88
Abstract_State => Platform_State,
9-
Initializes => (Platform_State, Main.Platform)
9+
Initializes => Platform_State
1010
is
1111

1212
procedure Construct (Cap : Gneiss.Capability) with

‎test/memory_client/gnat_ce_2020/component.ads

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
2+
with Gneiss_Internal;
3+
with Gneiss;
4+
with Gneiss.Component;
5+
6+
package Component with
7+
SPARK_Mode,
8+
Abstract_State => Platform_State,
9+
Initializes => (Platform_State, Main.Platform)
10+
is
11+
12+
procedure Construct (Cap : Gneiss.Capability) with
13+
Global => (In_Out => (Platform_State,
14+
Main.Platform,
15+
Gneiss_Internal.Platform_State));
16+
procedure Destruct with
17+
Global => (In_Out => (Platform_State,
18+
Gneiss_Internal.Platform_State));
19+
20+
package Main is new Gneiss.Component (Construct, Destruct);
21+
22+
end Component;

‎test/memory_server.gpr

+10-1
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,19 @@
11

22
project Memory_Server extends "gneiss_component" is
33

4+
Src_Dirs := ("memory_server");
5+
6+
case GCC_Version is
7+
when "9" =>
8+
Src_Dirs := ("memory_server/gnat_ce_2020") & Src_Dirs;
9+
when others =>
10+
null;
11+
end case;
12+
413
case Build_Step is
514
when "compile" =>
615
for Runtime ("Ada") use Gneiss_Runtime;
7-
for Source_Dirs use ("memory_server");
16+
for Source_Dirs use Src_Dirs;
817
for Object_Dir use external ("CEMENT_OBJECT_DIR");
918
for Library_Name use Gneiss_Component_Prefix & "memory_server";
1019
for Library_Kind use "dynamic";

‎test/memory_server/component.ads

+2-2
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,9 @@ with Gneiss.Component;
44
with Gneiss_Internal;
55

66
package Component with
7-
SPARK_Mode,
7+
SPARK_Mode,
88
Abstract_State => (Component_State, Platform_State),
9-
Initializes => (Platform_State, Main.Platform)
9+
Initializes => Platform_State
1010
is
1111

1212
procedure Construct (Cap : Gneiss.Capability) with

‎test/memory_server/gnat_ce_2020/component.ads

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
2+
with Gneiss;
3+
with Gneiss.Component;
4+
with Gneiss_Internal;
5+
6+
package Component with
7+
SPARK_Mode,
8+
Abstract_State => (Component_State, Platform_State),
9+
Initializes => (Platform_State, Main.Platform)
10+
is
11+
12+
procedure Construct (Cap : Gneiss.Capability) with
13+
Global => (Output => Component_State,
14+
In_Out => (Platform_State,
15+
Main.Platform,
16+
Gneiss_Internal.Platform_State));
17+
18+
procedure Destruct with
19+
Global => null;
20+
21+
package Main is new Gneiss.Component (Construct, Destruct);
22+
23+
end Component;

‎test/message_client.gpr

+10-1
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,19 @@
11

22
project Message_Client extends "gneiss_component" is
33

4+
Src_Dirs := ("message_client");
5+
6+
case GCC_Version is
7+
when "9" =>
8+
Src_Dirs := ("message_client/gnat_ce_2020") & Src_Dirs;
9+
when others =>
10+
null;
11+
end case;
12+
413
case Build_Step is
514
when "compile" =>
615
for Runtime ("Ada") use Gneiss_Runtime;
7-
for Source_Dirs use ("message_client");
16+
for Source_Dirs use Src_Dirs;
817
for Object_Dir use external ("CEMENT_OBJECT_DIR");
918
for Library_Name use Gneiss_Component_Prefix & "message_client";
1019
for Library_Kind use "dynamic";

‎test/message_client/component.ads

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ with Gneiss_Internal;
66
package Component with
77
SPARK_Mode,
88
Abstract_State => (Component_State, Platform_State),
9-
Initializes => (Platform_State, Main.Platform)
9+
Initializes => Platform_State
1010
is
1111

1212
procedure Construct (Cap : Gneiss.Capability) with

‎test/message_client/gnat_ce_2020/component.ads

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
2+
with Gneiss;
3+
with Gneiss.Component;
4+
with Gneiss_Internal;
5+
6+
package Component with
7+
SPARK_Mode,
8+
Abstract_State => (Component_State, Platform_State),
9+
Initializes => (Platform_State, Main.Platform)
10+
is
11+
12+
procedure Construct (Cap : Gneiss.Capability) with
13+
Global => (Output => Component_State,
14+
In_Out => (Platform_State,
15+
Main.Platform,
16+
Gneiss_Internal.Platform_State));
17+
18+
procedure Destruct with
19+
Global => (In_Out => (Platform_State, Gneiss_Internal.Platform_State));
20+
21+
package Main is new Gneiss.Component (Construct, Destruct);
22+
23+
end Component;

‎test/message_server.gpr

+10-1
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,20 @@
11

22
project Message_Server extends "gneiss_component" is
33

4+
Src_Dirs := ("message_server");
5+
6+
case GCC_Version is
7+
when "9" =>
8+
Src_Dirs := ("message_server/gnat_ce_2020") & Src_Dirs;
9+
when others =>
10+
null;
11+
end case;
12+
413
case Build_Step is
514
when "compile" =>
615
for Languages use ("Ada", "C");
716
for Runtime ("Ada") use Gneiss_Runtime;
8-
for Source_Dirs use ("message_server");
17+
for Source_Dirs use Src_Dirs;
918
for Object_Dir use external ("CEMENT_OBJECT_DIR");
1019
for Library_Name use Gneiss_Component_Prefix & "message_server";
1120
for Library_Kind use "dynamic";

‎test/message_server/component.ads

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ with Gneiss_Internal;
66
package Component with
77
SPARK_Mode,
88
Abstract_State => (Component_State, Platform_State),
9-
Initializes => (Platform_State, Main.Platform)
9+
Initializes => Platform_State
1010
is
1111

1212
procedure Construct (Cap : Gneiss.Capability) with

0 commit comments

Comments
 (0)
This repository has been archived.