diff --git a/src/plugins/e-acsl/examples/ensuresec/.gitignore b/src/plugins/e-acsl/examples/ensuresec/.gitignore
index 567609b1234a9b8806c5a05da6c866e480aa148d..624a0d90452b7edfc6a43b3a7409e123d5dd0ac3 100644
--- a/src/plugins/e-acsl/examples/ensuresec/.gitignore
+++ b/src/plugins/e-acsl/examples/ensuresec/.gitignore
@@ -1 +1,3 @@
build/
+__pycache__/
+.env
\ No newline at end of file
diff --git a/src/plugins/e-acsl/examples/ensuresec/Makefile b/src/plugins/e-acsl/examples/ensuresec/Makefile
index b60655a15f460b7785aade35fcee74c0ef119e16..1340456c4168f743659a39a2e65f0ac8954d863d 100644
--- a/src/plugins/e-acsl/examples/ensuresec/Makefile
+++ b/src/plugins/e-acsl/examples/ensuresec/Makefile
@@ -1,37 +1,26 @@
-OUT:=$(dir $(abspath $(lastword $(MAKEFILE_LIST))))build
-DEPS:=Makefile ensuresec_ee.c json_assert.c
-EACSL_CC:=e-acsl-gcc.sh -c --concurrency --external-assert json_assert.c ensuresec_ee.c
-MKDIR:=mkdir -p
-
-EE_ID:=EnsuresecEE
-EE_TOOL_ID:=EnsuresecEE_EACSL
-
-$(OUT)/ensuresec_ee.e-acsl: $(DEPS)
- $(MKDIR) $(OUT)
- $(EACSL_CC) -o $(OUT)/ensuresec_ee.frama.c -O $(OUT)/ensuresec_ee
-
-$(OUT)/ensuresec_ee_pall.e-acsl: $(DEPS)
- $(MKDIR) $(OUT)
- $(EACSL_CC) -e -DE_ACSL_DEBUG_ASSERT -o $(OUT)/ensuresec_ee_pall.frama.c -O $(OUT)/ensuresec_ee_pall
-
-$(OUT)/ensuresec_ee_debug.e-acsl: $(DEPS)
- $(MKDIR) $(OUT)
- $(EACSL_CC) -e -DE_ACSL_DEBUG_ASSERT --rt-debug -o $(OUT)/ensuresec_ee_debug.frama.c -O $(OUT)/ensuresec_ee_debug
-
-compile: $(OUT)/ensuresec_ee.e-acsl
-compile_print_all: $(OUT)/ensuresec_ee_pall.e-acsl
-compile_debug: $(OUT)/ensuresec_ee_debug.e-acsl
-
-run: $(OUT)/ensuresec_ee.e-acsl
- ENSURESEC_EE_ID="$(EE_ID)" ENSURESEC_EE_TOOL_ID="$(EE_TOOL_ID)" ENSURESEC_OUTPUT_FILE="$(OUT)/ensuresec_ee.json" $(OUT)/ensuresec_ee.e-acsl
-
-run_print_all: $(OUT)/ensuresec_ee_pall.e-acsl
- ENSURESEC_EE_ID="$(EE_ID)" ENSURESEC_EE_TOOL_ID="$(EE_TOOL_ID)" ENSURESEC_OUTPUT_FILE="$(OUT)/ensuresec_ee_pall.json" $(OUT)/ensuresec_ee_pall.e-acsl
-
-run_debug: $(OUT)/ensuresec_ee_debug.e-acsl
- ENSURESEC_EE_ID="$(EE_ID)" ENSURESEC_EE_TOOL_ID="$(EE_TOOL_ID)" ENSURESEC_OUTPUT_FILE="$(OUT)/ensuresec_ee_debug.json" $(OUT)/ensuresec_ee_debug.e-acsl
-
-all: run run_print_all run_debug
-
-clean:
- rm -rf $(OUT)
+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
diff --git a/src/plugins/e-acsl/examples/ensuresec/README.md b/src/plugins/e-acsl/examples/ensuresec/README.md
index 8192e73e7fb379db2c224eacebbb0dc0dce17d3f..5a74c0ef86eb167a1d1cb185f8cb14d4aebf4237 100644
--- a/src/plugins/e-acsl/examples/ensuresec/README.md
+++ b/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`
diff --git a/src/plugins/e-acsl/examples/ensuresec/json-output/Makefile b/src/plugins/e-acsl/examples/ensuresec/json-output/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..b60655a15f460b7785aade35fcee74c0ef119e16
--- /dev/null
+++ b/src/plugins/e-acsl/examples/ensuresec/json-output/Makefile
@@ -0,0 +1,37 @@
+OUT:=$(dir $(abspath $(lastword $(MAKEFILE_LIST))))build
+DEPS:=Makefile ensuresec_ee.c json_assert.c
+EACSL_CC:=e-acsl-gcc.sh -c --concurrency --external-assert json_assert.c ensuresec_ee.c
+MKDIR:=mkdir -p
+
+EE_ID:=EnsuresecEE
+EE_TOOL_ID:=EnsuresecEE_EACSL
+
+$(OUT)/ensuresec_ee.e-acsl: $(DEPS)
+ $(MKDIR) $(OUT)
+ $(EACSL_CC) -o $(OUT)/ensuresec_ee.frama.c -O $(OUT)/ensuresec_ee
+
+$(OUT)/ensuresec_ee_pall.e-acsl: $(DEPS)
+ $(MKDIR) $(OUT)
+ $(EACSL_CC) -e -DE_ACSL_DEBUG_ASSERT -o $(OUT)/ensuresec_ee_pall.frama.c -O $(OUT)/ensuresec_ee_pall
+
+$(OUT)/ensuresec_ee_debug.e-acsl: $(DEPS)
+ $(MKDIR) $(OUT)
+ $(EACSL_CC) -e -DE_ACSL_DEBUG_ASSERT --rt-debug -o $(OUT)/ensuresec_ee_debug.frama.c -O $(OUT)/ensuresec_ee_debug
+
+compile: $(OUT)/ensuresec_ee.e-acsl
+compile_print_all: $(OUT)/ensuresec_ee_pall.e-acsl
+compile_debug: $(OUT)/ensuresec_ee_debug.e-acsl
+
+run: $(OUT)/ensuresec_ee.e-acsl
+ ENSURESEC_EE_ID="$(EE_ID)" ENSURESEC_EE_TOOL_ID="$(EE_TOOL_ID)" ENSURESEC_OUTPUT_FILE="$(OUT)/ensuresec_ee.json" $(OUT)/ensuresec_ee.e-acsl
+
+run_print_all: $(OUT)/ensuresec_ee_pall.e-acsl
+ ENSURESEC_EE_ID="$(EE_ID)" ENSURESEC_EE_TOOL_ID="$(EE_TOOL_ID)" ENSURESEC_OUTPUT_FILE="$(OUT)/ensuresec_ee_pall.json" $(OUT)/ensuresec_ee_pall.e-acsl
+
+run_debug: $(OUT)/ensuresec_ee_debug.e-acsl
+ ENSURESEC_EE_ID="$(EE_ID)" ENSURESEC_EE_TOOL_ID="$(EE_TOOL_ID)" ENSURESEC_OUTPUT_FILE="$(OUT)/ensuresec_ee_debug.json" $(OUT)/ensuresec_ee_debug.e-acsl
+
+all: run run_print_all run_debug
+
+clean:
+ rm -rf $(OUT)
diff --git a/src/plugins/e-acsl/examples/ensuresec/ensuresec_ee.c b/src/plugins/e-acsl/examples/ensuresec/json-output/ensuresec_ee.c
similarity index 99%
rename from src/plugins/e-acsl/examples/ensuresec/ensuresec_ee.c
rename to src/plugins/e-acsl/examples/ensuresec/json-output/ensuresec_ee.c
index 310c49c1c6cad0df52d8a1f26deee6c2b4abad93..783b66df8b4fb57fd4d65f7dfdd73b21878b1187 100644
--- a/src/plugins/e-acsl/examples/ensuresec/ensuresec_ee.c
+++ b/src/plugins/e-acsl/examples/ensuresec/json-output/ensuresec_ee.c
@@ -89,7 +89,7 @@ static void *read_value(void *arg) {
usleep(100);
} while (!idx_written);
- // Acquire a read lock so that the specification can check `writte[idx]` and
+ // Acquire a read lock so that the specification can check `written[idx]` and
// `values[idx]`.
pthread_rwlock_rdlock(lock);
/*@ requires written[idx] == 1;
diff --git a/src/plugins/e-acsl/examples/ensuresec/json_assert.c b/src/plugins/e-acsl/examples/ensuresec/json-output/json_assert.c
similarity index 100%
rename from src/plugins/e-acsl/examples/ensuresec/json_assert.c
rename to src/plugins/e-acsl/examples/ensuresec/json-output/json_assert.c
diff --git a/src/plugins/e-acsl/examples/ensuresec/push-alerts/.env-example b/src/plugins/e-acsl/examples/ensuresec/push-alerts/.env-example
new file mode 100644
index 0000000000000000000000000000000000000000..8c1f90d40504e32b7c6847cdf9841037a4c7afe0
--- /dev/null
+++ b/src/plugins/e-acsl/examples/ensuresec/push-alerts/.env-example
@@ -0,0 +1,3 @@
+ENSURESEC_ALERT_URL="http://localhost:5000/alert"
+ENSURESEC_EE_ID="EnsuresecEE"
+ENSURESEC_EE_TOOL_ID="EnsuresecEE_EACSL"
diff --git a/src/plugins/e-acsl/examples/ensuresec/push-alerts/receiver.py b/src/plugins/e-acsl/examples/ensuresec/push-alerts/receiver.py
new file mode 100644
index 0000000000000000000000000000000000000000..78ccf80c64866a404159ed0319f0d29989bdecc6
--- /dev/null
+++ b/src/plugins/e-acsl/examples/ensuresec/push-alerts/receiver.py
@@ -0,0 +1,36 @@
+# -*- coding: utf-8 -*-
+
+# Test server that listen on URL /alert for JSON emitted by a program monitored
+# by E-ACSL and print received alerts to the console output.
+# Run with `FLASK_APP=receiver.py FLASK_ENV=development flask run`
+
+from flask import Flask, request
+
+app = Flask(__name__)
+
+
+@app.post("/alert")
+def add_alert():
+ if request.is_json:
+ alert = request.get_json()
+ content = alert['alert']['data'][0]['jsonContent']
+ print(
+"""{file}: In function '{fct}'
+{file}:{line}: {kind} {verdict}:
+\t{name}{post_name}{predicate}"""
+ .format(
+ file=content['location']['file'],
+ fct=content['location']['function'],
+ line=content['location']['line'],
+ kind=content['kind'],
+ verdict=content['verdict'],
+ name=content['name'],
+ post_name=":\n\t" if content['name'] else "",
+ predicate=content['predicate']
+ ))
+ if content['values']:
+ print("\tWith values:")
+ for value in content['values']:
+ print("\t- {}: {}".format(value['name'], value['value']))
+ return {}, 201
+ return {"error": "Request must be JSON."}, 415
diff --git a/src/plugins/e-acsl/examples/ensuresec/push-alerts/wrapper.py b/src/plugins/e-acsl/examples/ensuresec/push-alerts/wrapper.py
new file mode 100755
index 0000000000000000000000000000000000000000..9116944eca0b079055dca0814f62f65cb8df80ab
--- /dev/null
+++ b/src/plugins/e-acsl/examples/ensuresec/push-alerts/wrapper.py
@@ -0,0 +1,111 @@
+#!/usr/bin/env python3
+# -*- coding: utf-8 -*-
+
+# Wrapper for an E-ACSL monitored executable that will POST each raised alert
+# to a specific URL.
+
+import argparse
+import dotenv
+import ijson
+import os
+import requests
+import subprocess
+
+ALERT_URL = 'ENSURESEC_ALERT_URL'
+EE_ID = 'ENSURESEC_EE_ID'
+EE_TOOL_ID = 'ENSURESEC_EE_TOOL_ID'
+
+
+def check_config(value, name):
+ """Check if the given value is empty and exit with an error message if that
+ is the case."""
+ if not value:
+ print("The '{}' option should be provided and not empty.".format(name))
+ exit(1)
+
+
+@ijson.coroutine
+def send_alert(url):
+ """send_alert() is a coroutine that will process E-ACSL alerts as they are
+ emitted by the program. The JSON alerts are POST-ed to the given URL."""
+ while True:
+ alert = (yield)
+ r = requests.post(url, json=alert)
+ if not r.ok:
+ print("Error while sending alert: " + r.text)
+
+
+def main():
+ default = {
+ # Default empty values
+ ALERT_URL: '',
+ EE_ID: '',
+ EE_TOOL_ID: '',
+ # Read configuration from .env file if it exists
+ **dotenv.dotenv_values(".env"),
+ # Overwrite with environment variables
+ **os.environ
+ }
+
+ # Parse script arguments
+ parser = argparse.ArgumentParser(
+ description="Wrapper for an E-ACSL monitored executable that will POST \
+ each raised alert to a specific URL.")
+ parser.add_argument(
+ 'program',
+ help="E-ACSL program to launch and monitor.")
+ parser.add_argument(
+ 'args',
+ help="Arguments for the E-ACSL program.",
+ nargs='*')
+ parser.add_argument(
+ '-u', '--alert-url',
+ help="URL where alerts raised by the E-ACSL program must be pushed, \
+ default to environment variable {}.".format(ALERT_URL),
+ metavar='url',
+ default=default[ALERT_URL],
+ dest='alert_url')
+ parser.add_argument(
+ '-i', '--id',
+ help="Ensuresec e-commerce ecosystem id, default to environment \
+ variable {}.".format(EE_ID),
+ metavar='id',
+ default=default[EE_ID],
+ dest='id')
+ parser.add_argument(
+ '-t', '--tool-id',
+ help="Ensuresec e-commerce ecosystem tool id, default to environment \
+ variable {}.".format(EE_TOOL_ID),
+ metavar="id",
+ default=default[EE_TOOL_ID],
+ dest='tool_id')
+ config = parser.parse_args()
+
+ # Check that all necessary configurations have been provided
+ check_config(config.alert_url, 'alert-url')
+ check_config(config.id, 'id')
+ check_config(config.tool_id, 'tool-id')
+
+ # Create an environment for the subprocess with the information either
+ # retrieved from the configuration or the script arguments, and setup
+ # JSON output to stdout
+ env = {'ENSURESEC_EE_ID': config.id,
+ 'ENSURESEC_EE_TOOL_ID': config.tool_id,
+ 'ENSURESEC_OUTPUT_FILE': '-'}
+ # Launch E-ACSL program as a subprocess
+ p = subprocess.Popen([config.program] + config.args, stdout=subprocess.PIPE,
+ env=env)
+
+ # Parse output of E-ACSL program as it is produced and use a coroutine to
+ # process JSON objects
+ coro = ijson.items_coro(send_alert(config.alert_url), 'item')
+ for chunk in p.stdout:
+ coro.send(chunk)
+ coro.close()
+
+ # Wait for the end of E-ACSL program
+ p.wait()
+
+
+if __name__ == "__main__":
+ main()