[eacsl] Update Ensuresec README and root Makefile

src/plugins/e-acsl/examples/ensuresec/Makefile

+JSON_OUTPUT_DIR=$(dir $(abspath $(lastword $(MAKEFILE_LIST))))json-output
+PUSH_ALERTS_DIR=$(dir $(abspath $(lastword $(MAKEFILE_LIST))))push-alerts
+
+compile:
+	make -C $(JSON_OUTPUT_DIR) compile
+
+run:
+	make -C $(JSON_OUTPUT_DIR) run
+
+launch_receiver:
+	FLASK_APP=$(PUSH_ALERTS_DIR)/receiver.py FLASK_ENV=development flask run
+
+run_wrapped: compile
+	$(PUSH_ALERTS_DIR)/wrapper.py \
+		--alert-url http://localhost:5000/alert \
+		--id EnsuresecEE \
+		--tool-id EnsuresecEE_EACSL \
+		$(JSON_OUTPUT_DIR)/build/ensuresec_ee.e-acsl
+
+run_wrapped_print_all:
+	make -C $(JSON_OUTPUT_DIR) compile_print_all
+	$(PUSH_ALERTS_DIR)/wrapper.py \
+		--alert-url http://localhost:5000/alert \
+		--id EnsuresecEE \
+		--tool-id EnsuresecEE_EACSL \
+		$(JSON_OUTPUT_DIR)/build/ensuresec_ee_pall.e-acsl

src/plugins/e-acsl/examples/ensuresec/README.md

@@ -3,9 +3,33 @@
 This folder illustrates the developments done for the European H2020 project
 Ensuresec.
 
+## Usage
+
+The `Makefile` in the root folder provides targets to launch some tests.
+
+- `compile`: Compile the example in folder `json-output`;
+- `run`: Run the example in folder `json-output`;
+- `launch_receiver`: Launch the test server in folder `push-alerts`;
+- `run_wrapped`: Run the example in folder `json-output` wrapped with the script
+  in folder `push-alerts`. The test server must be launched before executing
+  this target.
+- `run_wrapped_print_all`: Same than
+
+When using `make run`, the alerts raised by the example are saved to a JSON file
+in `./json-output/build/ensuresec_ee.json`.
+
+To test pushing alerts to a web API, `make launch_receiver` should be run in a
+secondary terminal. Then `make run_wrapped` can be executed in the primary
+terminal and alerts raised by the example should be visible on the receiver. The
+target `run_wrapped_print_all` will also push valid assertions.
+
 ## Files
 
-### `Makefile`
+### Folder `json-output`
+
+Custom E-ACSL assert to output alerts in a JSON file.
+
+#### `Makefile`
 
 The makefile in the folder provides some targets to test the ensuresec
 developments:
@@ -19,7 +43,7 @@ developments:
 - `run_print_all`: run the output of the `compile_print_all` step.
 - `run_debug`: run the output of the `compile_debug` step.
 
-### `json_assert.c`
+#### `json_assert.c`
 
 The file `json_assert.c` contains an external `__e_acsl_assert()` implementation
 that will print assertion violations to a json file.
@@ -31,8 +55,39 @@ implementation:
 - `ENSURESEC_EE_TOOL_ID`: Ensuresec e-commerce ecosystem tool id
 - `ENSURESEC_OUTPUT_FILE`: json output file
 
-### `ensuresec_ee.c`
+#### `ensuresec_ee.c`
 
 Multithread program serving as an exemple Ensuresec e-commerce ecosystem
 program. The program contains `check` assertions that will be violated during
 its execution without halting the program.
+
+### Folder `push-alerts`
+
+Example of wrapping script to push alerts emitted by the program in
+`json-output` to a specific URL.
+
+#### `wrapper.py`
+
+Wrapper for an E-ACSL monitored executable that will `POST` each raised alert to
+a specific URL. See `./wrapper.py -h` for how to use the script.
+
+Python dependencies:
+
+- `python-dotenv`
+- `python-ijson`
+- `python-requests`
+
+#### `.env-example`
+
+Example `.env` file with environment variables read by `wrapper.py`.
+
+#### `receiver.py`
+
+Test server that listen on URL `http://localhost:5000/alert` for JSON emitted by
+an E-ACSL monitored program and print received alerts to the console output.
+
+Run with `FLASK_APP=receiver.py FLASK_ENV=development flask run`
+
+Python dependencies:
+
+- `python-flask`