Add testing of DCCP example

Ref. eng/recordflux/RecordFlux#1362

.gitlab-ci.yml

@@ -361,6 +361,7 @@ verification_apps:
         - "ping"
         - "dhcp_client"
         - "spdm_responder"
+        - "dccp"
   script:
     - *update_timestamps_of_generated_code
     - *setup_gnat

Makefile

@@ -167,6 +167,7 @@ test_compilation:
 	$(MAKE) -C examples/apps/ping build
 	$(MAKE) -C examples/apps/dhcp_client build
 	$(MAKE) -C examples/apps/spdm_responder lib
+	$(MAKE) -C examples/apps/dccp build
 	$(PYTEST) tests/compilation
 	$(MAKE) -C tests/spark test NOPREFIX=1
 	$(MAKE) -C tests/spark clean
@@ -334,6 +335,7 @@ clean:
 	$(MAKE) -C examples/apps/ping clean
 	$(MAKE) -C examples/apps/dhcp_client clean
 	$(MAKE) -C examples/apps/spdm_responder clean
+	$(MAKE) -C examples/apps/dccp clean
 	$(MAKE) -C doc/language_reference clean
 	$(MAKE) -C doc/user_guide clean
 	$(MAKE) -C ide/vscode clean

examples/apps/dccp/Makefile

@@ -1,11 +1,34 @@
+include ../../../Makefile.common
+
+SPECS = $(wildcard specs/*.rflx)
+GENERATED = build/generated/rflx-dccp-packet.ads
+BIN = build/obj/dccp_client build/obj/dccp_server
+GRAPHS = graphs/DCCP_Option.svg graphs/DCCP_Packet.svg
+
 .PHONY: test build prove generate clean
 
-test:
+test: $(BIN)
+	rflx validate --coverage -v tests/samples/valid -- $(SPECS) DCCP::Packet
+	tests/run
 
-build:
+build: $(BIN)
 
-prove:
+prove: $(GNATPROVE_CACHE_DIR) $(GENERATED)
+	$(GNATPROVE) -Pdccp
 
-generate:
+generate: $(GENERATED) $(GRAPHS)
 
 clean:
+	rm -rf build
+
+$(GENERATED): $(SPECS) | build/generated
+	rflx generate -d build/generated $^
+
+build/generated:
+	mkdir -p build/generated
+
+$(BIN): $(GENERATED) $(wildcard build/generated/*)
+	gprbuild -Pdccp -Xgnat=$(GNAT)
+
+$(GRAPHS): $(SPECS)
+	rflx graph -d graphs $^

examples/apps/dccp/README.md

@@ -1,7 +1,5 @@
 # DCCP
 
-## Getting started
-
 This project provides a simplified example set for a DCCP specification with a "client" and "server" application. Additional details about what each application does are described below.
 
 ## DCCP Server
@@ -37,32 +35,32 @@ Once the client is running and prints out message status information, the server
 
 ## DCCP Specification
 
-RecordFlux was used to generate the "DCCP specification" for this project. Note that the DCCP protocol was **NOT** implemented in its entirety. The core of the protocol is the **Generic Header**; a fairly simple implementation of this is implemented in RecordFlux. A small portion of **Additional Fields** and **Options** are also implemented so as to align with the Wireshark sample data set. Additionally, the **Application Data Area** of the protocol is lightly implemented here based on Wireshark data.
+Note that the DCCP protocol was **NOT** implemented in its entirety. The core of the protocol is the **Generic Header**; a fairly simple implementation of this is implemented in RecordFlux. A small portion of **Additional Fields** and **Options** are also implemented so as to align with the Wireshark sample data set. Additionally, the **Application Data Area** of the protocol is lightly implemented here based on Wireshark data.
 
-The DCCP Specification file is located in the **\specs** folder of each application.
+The DCCP Specification file is located in the `specs` directory.
 
-The message graph (generated from the specification file) is located in the **\out** folder of each application. This provides a visual graph of the message itself, which can be useful for understanding and/or message interpretation.
+The message graph (generated from the specification file) is located in the `graphs` directory. This provides a visual graph of the message itself, which can be useful for understanding and/or message interpretation.
 
 ## HOWTO: Generate a Message Graph
 
 To generate a message graph using RecordFlux, locate the message spec and enter the following into the terminal window:
 
-`rflx graph -d ./out dccp.rflx`
+`rflx graph -d graphs specs/dccp.rflx`
 
-For the above, **out** is the output directory for the graph and **dccp.rflx** is the spec file.
+For the above, `graphs` is the output directory for the graph and `dccp.rflx` is the spec file.
 
 ## HOWTO: Generate Code Files from a Specification
 
 To generate code files for the RecordFlux specification, locate the message spec and enter the following into the terminal window:
 
-`rflx generate -d ./generated/ dccp.rflx`
+`rflx generate -d build/generated specs/dccp.rflx`
 
-For the above, **generated** is the output directory for the generated code files and **dccp.rflx** is the spec file.
+For the above, `build/generated` is the output directory for the generated code files and `dccp.rflx` is the spec file.
 
 ## HOWTO: Validate the Specification
 
 RecordFlux provides the ability to validate a message specification with real world files in a RAW format. To run validate and generate a corresponding report, locate the message spec and enter the following into the terminal window:
 
-`rflx validate --coverage -v ./test/valid/ dccp.rflx DCCP::Header`
+`rflx validate --coverage -v tests/samples/valid -- specs/dccp.rflx DCCP::Packet`
 
-For the above, **./test/valid** is the folder in which "valid" sample RAW files are located and **dccp.rflx** is the spec file.
+For the above, `tests/samples/valid` is the directory in which "valid" sample RAW files are located and `dccp.rflx` is the spec file.

examples/apps/dccp/dccp.gpr

@@ -0,0 +1,43 @@
+with "../../../defaults";
+
+project Build is
+
+   for Languages use ("RecordFlux", "Ada");
+   for Source_Dirs use ("src", "build/generated", "specs");
+   for Object_Dir use "build/obj";
+   for Create_Missing_Dirs use "True";
+   for Main use ("dccp_client.adb", "dccp_server.adb");
+
+   package Builder is
+      for Default_Switches ("Ada") use Defaults.Builder_Switches;
+      for Global_Configuration_Pragmas use "common.adc";
+   end Builder;
+
+   package Compiler is
+      for Driver ("RecordFlux") use "";
+      for Default_Switches ("Ada") use Defaults.Compiler_Switches;
+   end Compiler;
+
+   package Binder is
+      for Default_Switches ("Ada") use Defaults.Binder_Switches;
+   end Binder;
+
+   package Naming is
+      for Spec_Suffix ("RecordFlux") use ".rflx";
+   end Naming;
+
+   package RecordFlux is
+      for Output_Dir use "build/generated";
+   end RecordFlux;
+
+   package Prove is
+      for Proof_Switches ("Ada") use Defaults.Proof_Switches &
+         (
+            "--prover=z3,cvc5,altergo,colibri"
+         );
+      for Proof_Switches ("msg_write.adb") use ("--timeout=300", "--memlimit=5000");
+      for Proof_Switches ("rflx-dccp-packet.adb") use ("--timeout=360", "--memlimit=5000");
+      for Proof_Switches ("rflx-rflx_arithmetic.adb") use ("--timeout=120");
+   end Prove;
+
+end Build;