diff --git a/automation/eclair_analysis/ECLAIR/Set1.ecl b/automation/eclair_analysis/ECLAIR/Set1.ecl
new file mode 100644
index 0000000000..86b8e7e772
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/Set1.ecl
@@ -0,0 +1,59 @@
+-doc_begin="Set 1 of Xen MISRA C guidelines"
+-enable=MC3R1.R9.1
+-enable=MC3R1.R12.5
+-enable=MC3R1.R17.3
+-enable=MC3R1.R17.4
+-enable=MC3R1.R17.6
+-enable=MC3R1.R19.1
+-enable=MC3R1.R21.13
+-enable=MC3R1.R21.17
+-enable=MC3R1.R21.18
+-enable=MC3R1.R21.19
+-enable=MC3R1.R21.20
+-enable=MC3R1.R21.21
+-enable=MC3R1.R22.2
+-enable=MC3R1.R22.4
+-enable=MC3R1.R22.5
+-enable=MC3R1.R22.6
+-enable=MC3R1.D1.1
+-enable=MC3R1.D2.1
+-enable=MC3R1.D4.1
+-enable=MC3R1.D4.3
+-enable=MC3R1.D4.7
+-enable=MC3R1.D4.10
+-enable=MC3R1.D4.11
+-enable=MC3R1.D4.14
+-enable=MC3R1.R1.1
+-enable=MC3R1.R1.3
+-enable=MC3R1.R1.4
+-enable=MC3R1.R2.1
+-enable=MC3R1.R2.2
+-enable=MC3R1.R3.1
+-enable=MC3R1.R3.2
+-enable=MC3R1.R4.1
+-enable=MC3R1.R5.1
+-enable=MC3R1.R5.2
+-enable=MC3R1.R5.3
+-enable=MC3R1.R5.4
+-enable=MC3R1.R5.6
+-enable=MC3R1.R6.1
+-enable=MC3R1.R6.2
+-enable=MC3R1.R7.1
+-enable=MC3R1.R7.2
+-enable=MC3R1.R7.3
+-enable=MC3R1.R7.4
+-enable=MC3R1.R8.1
+-enable=MC3R1.R8.2
+-enable=MC3R1.R8.3
+-enable=MC3R1.R8.4
+-enable=MC3R1.R8.5
+-enable=MC3R1.R8.6
+-enable=MC3R1.R8.8
+-enable=MC3R1.R8.10
+-enable=MC3R1.R8.12
+-enable=MC3R1.R8.14
+-enable=MC3R1.R9.2
+-enable=MC3R1.R9.3
+-enable=MC3R1.R9.4
+-enable=MC3R1.R9.5
+-doc_end
diff --git a/automation/eclair_analysis/ECLAIR/Set2.ecl b/automation/eclair_analysis/ECLAIR/Set2.ecl
new file mode 100644
index 0000000000..7608335cf4
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/Set2.ecl
@@ -0,0 +1,25 @@
+-doc_begin="Set 2 of Xen MISRA C guidelines"
+-enable=MC3R1.R10.1
+-enable=MC3R1.R10.2
+-enable=MC3R1.R10.3
+-enable=MC3R1.R10.4
+-enable=MC3R1.R10.6
+-enable=MC3R1.R10.7
+-enable=MC3R1.R10.8
+-enable=MC3R1.R11.1
+-enable=MC3R1.R11.2
+-enable=MC3R1.R11.3
+-enable=MC3R1.R11.6
+-enable=MC3R1.R11.7
+-enable=MC3R1.R11.8
+-enable=MC3R1.R11.9
+-enable=MC3R1.R12.2
+-enable=MC3R1.R13.1
+-enable=MC3R1.R13.2
+-enable=MC3R1.R13.5
+-enable=MC3R1.R13.6
+-enable=MC3R1.R14.1
+-enable=MC3R1.R14.2
+-enable=MC3R1.R14.3
+-enable=MC3R1.R14.4
+-doc_end
diff --git a/automation/eclair_analysis/ECLAIR/Set3.ecl b/automation/eclair_analysis/ECLAIR/Set3.ecl
new file mode 100644
index 0000000000..d2c2c4b21f
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/Set3.ecl
@@ -0,0 +1,67 @@
+-doc_begin="Set 3 of Xen MISRA C guidelines"
+-enable=MC3R1.D4.12
+-enable=MC3R1.R5.5
+-enable=MC3R1.R5.7
+-enable=MC3R1.R5.8
+-enable=MC3R1.R15.2
+-enable=MC3R1.R15.3
+-enable=MC3R1.R15.6
+-enable=MC3R1.R15.7
+-enable=MC3R1.R16.1
+-enable=MC3R1.R16.2
+-enable=MC3R1.R16.3
+-enable=MC3R1.R16.4
+-enable=MC3R1.R16.5
+-enable=MC3R1.R16.6
+-enable=MC3R1.R16.7
+-enable=MC3R1.R17.1
+-enable=MC3R1.R17.2
+-enable=MC3R1.R17.5
+-enable=MC3R1.R17.7
+-enable=MC3R1.R18.1
+-enable=MC3R1.R18.2
+-enable=MC3R1.R18.3
+-enable=MC3R1.R18.6
+-enable=MC3R1.R18.7
+-enable=MC3R1.R18.8
+-enable=MC3R1.R20.2
+-enable=MC3R1.R20.3
+-enable=MC3R1.R20.4
+-enable=MC3R1.R20.6
+-enable=MC3R1.R20.7
+-enable=MC3R1.R20.8
+-enable=MC3R1.R20.9
+-enable=MC3R1.R20.11
+-enable=MC3R1.R20.12
+-enable=MC3R1.R20.13
+-enable=MC3R1.R20.14
+-enable=MC3R1.R21.1
+-enable=MC3R1.R21.2
+-enable=MC3R1.R21.3
+-enable=MC3R1.R21.4
+-enable=MC3R1.R21.5
+-enable=MC3R1.R21.6
+-enable=MC3R1.R21.7
+-enable=MC3R1.R21.8
+-enable=MC3R1.R21.9
+-enable=MC3R1.R21.10
+-enable=MC3R1.R21.12
+-enable=MC3R1.R21.14
+-enable=MC3R1.R21.15
+-enable=MC3R1.R21.16
+-enable=MC3R1.R22.1
+-enable=MC3R1.R22.3
+-enable=MC3R1.R22.7
+-enable=MC3R1.R22.8
+-enable=MC3R1.R22.9
+-enable=MC3R1.R22.10
+-enable=MC3R1.R2.6
+-enable=MC3R1.R4.2
+-doc_end
+
+-doc_begin="Guidelines added with Xen MISRA C Task (a): Xen Coding Guidelines v1.1, June 1, 2023"
+-enable=MC3R1.R21.11
+-enable=MC3R1.D4.4
+-enable=MC3R1.R8.9
+-enable=MC3R1.R12.4
+-doc_end
diff --git a/automation/eclair_analysis/ECLAIR/action.helpers b/automation/eclair_analysis/ECLAIR/action.helpers
new file mode 100644
index 0000000000..2ad6428eaa
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/action.helpers
@@ -0,0 +1,193 @@
+if [ -n "${GITLAB_CI:-}" ]; then
+    ci=gitlab
+elif [ -n "${GITHUB_ACTION:-}" ]; then
+    ci=github
+elif [ -n "${JENKINS_HOME:-}" ]; then
+    ci=jenkins
+else
+    echo "Unexpected CI/CD context" >&2
+    exit 1
+fi
+
+esc=$(printf '\e')
+cr=$(printf '\r')
+
+open_section() {
+    id=$1
+    title=$2
+    collapsed=$3
+    echo "${esc}[0Ksection_start:$(date +%s):${id}${collapsed}${cr}${esc}[0K${esc}[1m${esc}[36m${title}${esc}[m"
+}
+
+close_section() {
+    id=$1
+    echo "${esc}[0Ksection_end:$(date +%s):${id}${cr}${esc}[0K"
+}
+
+summary() {
+    fixedReports=
+    newReports=
+    unfixedReports=
+    while read -r line; do
+        var=${line%%: *}
+        val=${line#*: }
+        eval "${var}=${val}"
+    done <"${updateLog}"
+
+    case "${ci}" in
+    github)
+        nl="\\"
+        ;;
+    gitlab)
+        nl=
+        ;;
+    jenkins)
+        nl="<br/>"
+        ;;
+    *)
+        nl=
+        ;;
+    esac
+
+    if [ -z "${newReports}" ]; then
+        fixedMsg=
+        unfixedMsg="Unfixed reports: ${unfixedReports}"
+        countsMsg="${unfixedMsg}"
+    else
+        fixedMsg="Fixed reports: ${fixedReports}"
+        unfixedMsg="Unfixed reports: ${unfixedReports} [new: ${newReports}]"
+        countsMsg="${fixedMsg}${nl}
+${unfixedMsg}"
+    fi
+    case "${ci}" in
+    jenkins)
+        cat <<EOF >"${summaryTxt}"
+${countsMsg}                                                                              ${nl}
+<a href="https://www.bugseng.com/eclair">
+  <img src="${eclairReportUrlPrefix}/rsrc/eclair.svg" width="100" />
+</a>
+<h3>${jobHeadline}</h3>
+<a href="${indexHtmlUrl}">Browse analysis results</a>
+EOF
+        ;;
+    *)
+        cat <<EOF >"${summaryTxt}"
+<a href="https://www.bugseng.com/eclair">
+  <img src="${eclairReportUrlPrefix}/rsrc/eclair.svg" width="100" />
+</a>
+Analysis Summary
+
+${jobHeadline}${nl}
+${countsMsg}${nl}
+[Browse analysis](${indexHtmlUrl})
+EOF
+        ;;
+    esac
+
+    case ${ci} in
+    github)
+        cat "${summaryTxt}" >"${GITHUB_STEP_SUMMARY}"
+        ;;
+    gitlab)
+        open_section ECLAIR_summary "ECLAIR analysis summary" ""
+        # Generate summary and print it (GitLab-specific)
+        cat <<EOF
+${jobHeadline}
+${countsMsg}
+Browse analysis: ${esc}[33m${indexHtmlUrl}${esc}[m
+EOF
+        close_section ECLAIR_summary
+        ;;
+    jenkins)
+        cat <<EOF
+${jobHeadline}
+${fixedMsg}
+${unfixedMsg}
+Browse analysis: ${indexHtmlUrl}
+EOF
+        ;;
+    *)
+        echo "Unexpected CI/CD context" >&2
+        exit 1
+        ;;
+    esac
+}
+
+log_file() {
+    section_id=$1
+    section_name=$2
+    file=$3
+    exit_code=$4
+    if [ "${exit_code}" = 0 ]; then
+        collapsed=[collapsed=true]
+    else
+        collapsed=
+    fi
+
+    case ${ci} in
+    github | jenkins)
+        echo "${section_name}"
+        ;;
+    gitlab)
+        open_section "${section_id}" "${section_name}" "${collapsed}"
+        ;;
+    *)
+        echo "Unexpected CI/CD context" >&2
+        exit 1
+        ;;
+    esac
+
+    cat "${file}"
+
+    case ${ci} in
+    github | jenkins) ;;
+    gitlab)
+        close_section "${section_id}"
+        ;;
+    *) ;;
+    esac
+}
+
+maybe_log_file_exit() {
+    section_id=$1
+    section_name=$2
+    file=$3
+    exit_code=$4
+
+    case ${ci} in
+    github | jenkins)
+        echo "${section_name}"
+        ;;
+    gitlab)
+        open_section "${section_id}" "${section_name}" ""
+        ;;
+    *)
+        echo "Unexpected CI/CD context" >&2
+        exit 1
+        ;;
+    esac
+
+    if [ "${exit_code}" != 0 ]; then
+        cat "${file}"
+    fi
+
+    case ${ci} in
+    github | jenkins) ;;
+    gitlab)
+        close_section "${section_id}"
+        ;;
+    *) ;;
+    esac
+    return "${exit_code}"
+}
+
+is_enabled() {
+    case "$1" in
+    true | TRUE | y | Y | yes | YES | 1)
+        return 0
+        ;;
+    *)
+        return 1
+        ;;
+    esac
+}
diff --git a/automation/eclair_analysis/ECLAIR/action.settings b/automation/eclair_analysis/ECLAIR/action.settings
new file mode 100644
index 0000000000..96426811a8
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/action.settings
@@ -0,0 +1,172 @@
+variantSubDir=
+variantHeadline=
+if [ -n "${VARIANT:-}" ]; then
+    variantSubDir="/${VARIANT}"
+    variantHeadline=" [${VARIANT}]"
+fi
+
+# AUTO PR Feature
+# If the following variables are defined, then all pipelines
+# of other branches will be considered pull-requests to
+# autoPRBranch.
+# Customized
+autoPRRepository="${AUTO_PR_REPOSITORY:-}"
+# Customized
+autoPRBranch="${AUTO_PR_BRANCH:-}"
+
+# Customized
+artifactsRoot=/var/local/eclair
+
+case "${ci}" in
+github)
+    # To be customized
+    repository="${GITHUB_REPOSITORY}"
+    jobId="${GITHUB_RUN_NUMBER}"
+
+    autoPRRemoteUrl="${GITHUB_SERVER_URL}/${autoPRRepository:-}.git"
+
+    case "${GITHUB_EVENT_NAME}" in
+    pull_request*)
+        event=pull_request
+        pullRequestId="${GITHUB_EVENT_PULL_REQUEST_NUMBER}"
+        pullRequestHeadRepo="${PR_HEAD_REPO}"
+        pullRequestHeadRef="${PR_HEAD_REF}"
+        pullRequestBaseRef="${PR_BASE_REF}"
+        pullRequestUser="${PR_USER}"
+        # baseCommitId and headCommitId are the most recent merge points without conflicts
+        git fetch -q --deepen=2
+        baseCommitId=$(git show -s --pretty=%H HEAD^1)
+        headCommitId=$(git show -s --pretty=%H HEAD^2)
+        ;;
+    push | workflow_dispatch)
+        event=push
+        # Extract the branch name from "refs/heads/<branch>"
+        branch="${GITHUB_REF#refs/heads/}"
+        headCommitId="${GITHUB_SHA}"
+        pushUser="${GITHUB_ACTOR}"
+        ;;
+    *)
+        echo "Unexpected GITHUB_REF ${GITHUB_REF}" >&2
+        exit 1
+        ;;
+    esac
+    ;;
+gitlab)
+    # Customized
+    repository="${CI_PROJECT_PATH}"
+    jobId="${CI_JOB_ID}"
+
+    gitlabApiUrl="${CI_SERVER_PROTOCOL}://${CI_SERVER_HOST}:${CI_SERVER_PORT}/api/v4"
+    autoPRRemoteUrl="${CI_SERVER_PROTOCOL}://${CI_SERVER_HOST}:${CI_SERVER_PORT}/${autoPRRepository:-}.git"
+
+    # Customized
+    gitlabBotToken="${ECLAIR_BOT_TOKEN:-}"
+
+    case "${CI_PIPELINE_SOURCE}" in
+    merge_request_event)
+        event=pull_request
+        pullRequestId="${CI_MERGE_REQUEST_IID}"
+        pullRequestHeadRef="${CI_MERGE_REQUEST_SOURCE_BRANCH_NAME}"
+        pullRequestHeadRepo="${CI_MERGE_REQUEST_SOURCE_PROJECT_PATH}"
+        pullRequestBaseRef="${CI_MERGE_REQUEST_TARGET_BRANCH_NAME}"
+        pullRequestUser="${GITLAB_USER_LOGIN}"
+        headCommitId="${CI_COMMIT_SHA}"
+        baseCommitId="${CI_MERGE_REQUEST_DIFF_BASE_SHA}"
+        ;;
+    push | pipeline | web)
+        event=push
+        branch="${CI_COMMIT_BRANCH}"
+        headCommitId="${CI_COMMIT_SHA}"
+        pushUser="${GITLAB_USER_NAME}"
+        ;;
+    *)
+        echo "Unexpected event ${CI_PIPELINE_SOURCE}" >&2
+        exit 1
+        ;;
+    esac
+    ;;
+jenkins)
+    # To be customized
+    repository="${JOB_BASE_NAME}"
+    project="${JOB_NAME}"
+    jobId="${BUILD_NUMBER}"
+
+    jenkinsApiUrl="${JENKINS_URL}"
+    autoPRRemoteUrl="${JENKINS_URL}/${autoPRRepository:-}.git"
+
+    # To be customized
+    jenkinsBotUsername="${ECLAIR_BOT_USERNAME:-}"
+    jenkinsBotToken="${ECLAIR_BOT_TOKEN:-}"
+
+    event=push
+    branch="${GIT_BRANCH}"
+    headCommitId="${GIT_COMMIT}"
+    pushUser=$(git show --pretty='format:%aN' -s)
+    ;;
+*)
+    echo "Unexpected CI/CD context" >&2
+    exit 1
+    ;;
+esac
+
+if [ "${event}" = "push" ] && [ -n "${autoPRBranch:-}" ]; then
+    # AUTO PR Feature enabled
+    if ! [ "${branch}" = "${autoPRBranch}" ] ||
+        ! [ "${repository}" = "${autoPRRepository}" ]; then
+        event=auto_pull_request
+    fi
+fi
+
+case "${event}" in
+pull_request)
+    subDir="${pullRequestHeadRepo}.ecdf/${pullRequestBaseRef}"
+    jobHeadline="ECLAIR ${ANALYSIS_KIND} on repository ${repository}: ${pullRequestUser} wants to merge ${pullRequestHeadRepo}:${pullRequestHeadRef} (${headCommitId}) into ${pullRequestBaseRef} (${baseCommitId})"
+    ;;
+push)
+    subDir="${branch}"
+    jobHeadline="ECLAIR ${ANALYSIS_KIND} on repository ${repository}: branch ${branch} (${headCommitId})"
+    badgeLabel="ECLAIR ${ANALYSIS_KIND} ${branch}${variantHeadline} #${jobId}"
+    ;;
+auto_pull_request)
+    git remote remove autoPRRemote || true
+    git remote add autoPRRemote "${autoPRRemoteUrl}"
+    git fetch -q autoPRRemote
+    subDir="${branch}"
+    baseCommitId=$(git merge-base "autoPRRemote/${autoPRBranch}" HEAD)
+    jobHeadline="ECLAIR ${ANALYSIS_KIND} on repository ${repository}: ${pushUser} wants to merge ${repository}:${branch} (${headCommitId}) into ${autoPRRepository}/${autoPRBranch} (${baseCommitId})"
+    ;;
+*)
+    echo "Unexpected event ${event}" >&2
+    exit 1
+    ;;
+esac
+
+case "${repository}" in
+xen-project/xen)
+    # Customized
+    keepOldAnalyses=0
+    ;;
+xen-project/*)
+    # Customized
+    keepOldAnalyses=10
+    ;;
+*)
+    echo "Unexpected repository" >&2
+    exit 1
+    ;;
+esac
+
+ECLAIR_BIN_DIR=/opt/bugseng/eclair/bin/
+
+artifactsDir="${artifactsRoot}/xen-project.ecdf/${repository}/ECLAIR_${ANALYSIS_KIND}"
+subDir="${subDir}${variantSubDir}"
+jobHeadline="${jobHeadline}${variantHeadline}"
+
+# Customized
+eclairReportUrlPrefix=https://saas.eclairit.com:3787
+
+jobDir="${artifactsDir}/${subDir}/${jobId}"
+updateLog="${analysisOutputDir}/update.log"
+commentLog="${analysisOutputDir}/comment.json"
+indexHtmlUrl="${eclairReportUrlPrefix}/fs${jobDir}/index.html"
+summaryTxt="${analysisOutputDir}/summary.txt"
diff --git a/automation/eclair_analysis/ECLAIR/action_clean_added.sh b/automation/eclair_analysis/ECLAIR/action_clean_added.sh
new file mode 100755
index 0000000000..59bc35fd13
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/action_clean_added.sh
@@ -0,0 +1,36 @@
+#!/bin/sh
+
+set -eu
+
+usage() {
+    echo "Usage: $0 ANALYSIS_OUTPUT_DIR" >&2
+    exit 2
+}
+
+[ $# -eq 1 ] || usage
+
+analysisOutputDir=$1
+
+cleanAddedTxt="${analysisOutputDir}/clean_added.log"
+
+# Load settings and helpers
+. "$(dirname "$0")/action.helpers"
+. "$(dirname "$0")/action.settings"
+
+unexpectedReports=$("${ECLAIR_BIN_DIR}eclair_report" \
+    "-db='${analysisOutputDir}/PROJECT.ecd'" \
+    "-sel_unfixed=unfixed" \
+    "-sel_tag_glob=clean_added,clean,added" \
+    "-print='',reports_count()")
+
+if [ "${unexpectedReports}" -gt 0 ]; then
+    cat <<EOF >"${cleanAddedTxt}"
+Failure: ${unexpectedReports} unexpected reports found.
+Unexpected reports are tagged 'clean:added'.
+EOF
+    exit 1
+else
+    cat <<EOF >"${cleanAddedTxt}"
+Success: No unexpected reports.
+EOF
+fi
diff --git a/automation/eclair_analysis/ECLAIR/action_log.sh b/automation/eclair_analysis/ECLAIR/action_log.sh
new file mode 100755
index 0000000000..67125b08f3
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/action_log.sh
@@ -0,0 +1,15 @@
+#!/bin/sh
+
+set -eu
+
+usage() {
+    echo "Usage: $0 SECTION_ID SECTION_NAME FILE EXIT_CODE" >&2
+    exit 2
+}
+
+[ $# -eq 4 ] || usage
+
+# Load settings and helpers
+. "$(dirname "$0")/action.helpers"
+
+log_file "$@"
diff --git a/automation/eclair_analysis/ECLAIR/action_pull_request.sh b/automation/eclair_analysis/ECLAIR/action_pull_request.sh
new file mode 100644
index 0000000000..68f7e6282e
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/action_pull_request.sh
@@ -0,0 +1,57 @@
+#!/bin/sh
+
+set -eu
+
+usage() {
+    echo "Usage: $0 WTOKEN ANALYSIS_OUTPUT_DIR COMMIT_ID" >&2
+    exit 2
+}
+
+[ $# -eq 2 ] || usage
+
+wtoken=$1
+analysisOutputDir=$2
+
+# Load settings and helpers
+. "$(dirname "$0")/action.helpers"
+. "$(dirname "$0")/action.settings"
+
+curl -sS "${eclairReportUrlPrefix}/ext/update_pull_request" \
+    -F "wtoken=${wtoken}" \
+    -F "artifactsDir=${artifactsDir}" \
+    -F "subDir=${subDir}" \
+    -F "jobId=${jobId}" \
+    -F "jobHeadline=${jobHeadline}" \
+    -F "baseCommitId=${baseCommitId}" \
+    -F "keepOldAnalyses=${keepOldAnalyses}" \
+    -F "db=@${analysisOutputDir}/PROJECT.ecd" \
+    >"${updateLog}"
+ex=0
+grep -Fq "unfixedReports: " "${updateLog}" || ex=$?
+maybe_log_file_exit PUBLISH_RESULT "Publishing results" "${updateLog}" "${ex}"
+
+summary
+
+if is_enabled "${ENABLE_ECLAIR_BOT:-}"; then
+    case ${ci} in
+    github)
+        ex=0
+        gh api \
+            --method POST \
+            "/repos/${repository}/issues/${pullRequestId}/comments" \
+            -F "body=@${summaryTxt}" \
+            --silent >"${commentLog}" 2>&1 || ex=$?
+        maybe_log_file_exit ADD_COMMENT "Adding comment" "${commentLog}" "${ex}"
+        ;;
+    gitlab)
+        curl -sS --request POST \
+            "${gitlabApiUrl}/projects/${CI_PROJECT_ID}/merge_requests/${pullRequestId}/notes" \
+            -H "PRIVATE-TOKEN: ${gitlabBotToken}" \
+            -F "body=<${summaryTxt}" >"${commentLog}"
+        ex=0
+        grep -Fq "Unfixed reports: " "${commentLog}" || ex=$?
+        maybe_log_file_exit ADD_COMMENT "Adding comment" "${commentLog}" "${ex}"
+        ;;
+    *) ;;
+    esac
+fi
diff --git a/automation/eclair_analysis/ECLAIR/action_push.sh b/automation/eclair_analysis/ECLAIR/action_push.sh
new file mode 100755
index 0000000000..45215fbf00
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/action_push.sh
@@ -0,0 +1,95 @@
+#!/bin/sh
+
+set -eu
+
+usage() {
+    echo "Usage: $0 WTOKEN ANALYSIS_OUTPUT_DIR" >&2
+    exit 2
+}
+
+[ $# -eq 2 ] || usage
+
+wtoken=$1
+analysisOutputDir=$2
+
+# Load settings and helpers
+. "$(dirname "$0")/action.helpers"
+. "$(dirname "$0")/action.settings"
+
+case "${event}" in
+push)
+    curl -sS "${eclairReportUrlPrefix}/ext/update_push" \
+        -F "wtoken=${wtoken}" \
+        -F "artifactsDir=${artifactsDir}" \
+        -F "subDir=${subDir}" \
+        -F "jobId=${jobId}" \
+        -F "jobHeadline=${jobHeadline}" \
+        -F "commitId=${headCommitId}" \
+        -F "badgeLabel=${badgeLabel}" \
+        -F "keepOldAnalyses=${keepOldAnalyses}" \
+        -F "db=@${analysisOutputDir}/PROJECT.ecd" \
+        >"${updateLog}"
+    ;;
+auto_pull_request)
+    curl -sS "${eclairReportUrlPrefix}/ext/update_pull_request" \
+        -F "wtoken=${wtoken}" \
+        -F "artifactsDir=${artifactsDir}" \
+        -F "subDir=${subDir}" \
+        -F "jobId=${jobId}" \
+        -F "jobHeadline=${jobHeadline}" \
+        -F "baseCommitId=${baseCommitId}" \
+        -F "keepOldAnalyses=${keepOldAnalyses}" \
+        -F "db=@${analysisOutputDir}/PROJECT.ecd" \
+        >"${updateLog}"
+    ;;
+*)
+    echo "Unexpected event ${event}" >&2
+    exit 1
+    ;;
+esac
+
+ex=0
+grep -Fq "unfixedReports: " "${updateLog}" || ex=$?
+maybe_log_file_exit PUBLISH_RESULT "Publishing results" "${updateLog}" "${ex}"
+
+summary
+
+if is_enabled "${ENABLE_ECLAIR_BOT:-}"; then
+    case ${ci} in
+    github)
+        ex=0
+        gh api \
+            --method POST \
+            "/repos/${repository}/commits/${headCommitId}/comments" \
+            -F "body=@${summaryTxt}" \
+            --silent >"${commentLog}" 2>&1 || ex=$?
+        maybe_log_file_exit ADD_COMMENT "Adding comment" "${commentLog}" "${ex}"
+        ;;
+    gitlab)
+        curl -sS --request POST \
+            "${gitlabApiUrl}/projects/${CI_PROJECT_ID}/repository/commits/${CI_COMMIT_SHA}/comments" \
+            -H "PRIVATE-TOKEN: ${gitlabBotToken}" \
+            -F "note=<${summaryTxt}" >"${commentLog}"
+        ex=0
+        grep -Fq "Unfixed reports: " "${commentLog}" || ex=$?
+        maybe_log_file_exit ADD_COMMENT "Adding comment" "${commentLog}" "${ex}"
+        ;;
+    jenkins)
+        ex=0
+        curl \
+            --user "${jenkinsBotUsername}:${jenkinsBotToken}" \
+            --data-urlencode "description=$(cat "${summaryTxt}")" \
+            --data-urlencode "Submit=Submit" \
+            "${jenkinsApiUrl}job/${project}/${jobId}/submitDescription" \
+            >"${commentLog}" 2>&1 || ex=$?
+        curl \
+            --user "${jenkinsBotUsername}:${jenkinsBotToken}" \
+            --data-urlencode "description=$(cat "${summaryTxt}")" \
+            --data-urlencode "Submit=Submit" \
+            "${jenkinsApiUrl}job/${project}/submitDescription" \
+            >"${commentLog}" 2>&1 || ex=$?
+        maybe_log_file_exit ADD_COMMENT "Adding comment" "${commentLog}" "${ex}"
+        ;;
+    *) ;;
+    esac
+fi
diff --git a/automation/eclair_analysis/ECLAIR/action_upload_sarif.sh b/automation/eclair_analysis/ECLAIR/action_upload_sarif.sh
new file mode 100755
index 0000000000..60b8034fcc
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/action_upload_sarif.sh
@@ -0,0 +1,31 @@
+#!/bin/sh
+
+set -eu
+
+usage() {
+    echo "Usage: $0 SARIF_FILE" >&2
+    exit 2
+}
+
+[ $# -eq 1 ] || usage
+
+HERE=$( (
+    cd "$(dirname "$0")"
+    echo "${PWD}"
+))
+
+. "${HERE}/action.helpers"
+
+sarifFile=$1
+sarifPayload=${HERE}/sarif.gz.b64
+uploadLog=${HERE}/upload_sarif.log
+
+gzip -c "${sarifFile}" | base64 -w0 >"${sarifPayload}"
+
+ex=0
+gh api --method POST -H "Accept: application/vnd.github+json" \
+    "/repos/${GITHUB_REPOSITORY}/code-scanning/sarifs" \
+    -f "commit_sha=${GITHUB_SHA}" -f "ref=${GITHUB_REF}" \
+    -F "sarif=@${sarifPayload}" \
+    --silent >"${uploadLog}" 2>&1 || ex=$?
+maybe_log_file_exit ADD_COMMENT "Uploading SARIF" "${uploadLog}" "${ex}"
diff --git a/automation/eclair_analysis/ECLAIR/analysis.ecl b/automation/eclair_analysis/ECLAIR/analysis.ecl
new file mode 100644
index 0000000000..fe418d6da1
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/analysis.ecl
@@ -0,0 +1,25 @@
+-setq=set,getenv("SET")
+-project_name=getenv("ECLAIR_PROJECT_NAME")
+-project_root=getenv("ECLAIR_PROJECT_ROOT")
+
+-setq=data_dir,getenv("ECLAIR_DATA_DIR")
+
+-verbose
+
+-enable=B.REPORT.ECB
+-config=B.REPORT.ECB,output=join_paths(data_dir,"FRAME.@FRAME@.ecb")
+-config=B.REPORT.ECB,preprocessed=show
+-config=B.REPORT.ECB,macros=10
+
+-enable=B.EXPLAIN
+
+-eval_file=toolchain.ecl
+-eval_file=public_APIs.ecl
+-eval_file=out_of_scope.ecl
+-eval_file=deviations.ecl
+-eval_file=call_properties.ecl
+-eval_file=tagging.ecl
+-eval_file=concat(set,".ecl")
+
+-doc="Hide reports in external code."
+-reports+={hide,all_exp_external}
diff --git a/automation/eclair_analysis/ECLAIR/analyze.sh b/automation/eclair_analysis/ECLAIR/analyze.sh
new file mode 100755
index 0000000000..47cdbb03ce
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/analyze.sh
@@ -0,0 +1,106 @@
+#!/bin/bash
+# Stop immediately if any executed command has exit status different from 0.
+set -e
+set -o pipefail
+
+script_name="$(basename "$0")"
+
+fatal() {
+  echo "${script_name}: $*" >&2
+  exit 1
+}
+
+usage() {
+  fatal "Usage: ${script_name} <ARM64|X86_64> <Set0|Set1|Set2|Set3>"
+}
+
+if [[ $# -ne 2 ]]; then
+  usage
+fi
+
+# Absolute path of the ECLAIR bin directory.
+export ECLAIR_BIN_DIR=/opt/bugseng/eclair/bin/
+
+# Directory where this script resides: usually in a directory named "ECLAIR".
+SCRIPT_DIR="$(
+  cd "$(dirname "$0")"
+  echo "${PWD}"
+)"
+# Directory where to put all ECLAIR output and temporary files.
+if [[ -z "${ECLAIR_OUTPUT_DIR:-}" ]]; then
+  ECLAIR_OUTPUT_DIR="${PWD}/ECLAIR/out"
+fi
+
+export ECLAIR_DIAGNOSTICS_OUTPUT="${ECLAIR_OUTPUT_DIR}/ANALYSIS.log"
+# Set the variable for the build log file.
+ECLAIR_BUILD_LOG=${ECLAIR_OUTPUT_DIR}/BUILD.log
+# Set the variable for the report log file.
+ECLAIR_REPORT_LOG=${ECLAIR_OUTPUT_DIR}/REPORT.log
+
+if [[ "$1" = "X86_64" ]]; then
+  export CROSS_COMPILE=
+  export XEN_TARGET_ARCH=x86_64
+  EXTRA_ECLAIR_ENV_OPTIONS=-disable=MC3R1.R20.7
+elif [[ "$1" = "ARM64" ]]; then
+  export CROSS_COMPILE=aarch64-linux-gnu-
+  export XEN_TARGET_ARCH=arm64
+else
+  fatal "Unknown configuration: $1"
+fi
+
+VARIANT="${XEN_TARGET_ARCH}"
+
+# Used in analysis.ecl
+case "$2" in
+Set0|Set1|Set2|Set3)
+  export SET="$2"
+  ;;
+*)
+  fatal "Unknown configuration: $2"
+  ;;
+esac
+
+export CC_ALIASES="${CROSS_COMPILE}gcc-12"
+export CXX_ALIASES="${CROSS_COMPILE}g++-12"
+export LD_ALIASES="${CROSS_COMPILE}ld"
+export AR_ALIASES="${CROSS_COMPILE}ar"
+export AS_ALIASES="${CROSS_COMPILE}as"
+export FILEMANIP_ALIASES="cp mv ${CROSS_COMPILE}objcopy"
+
+# ECLAIR binary data directory and workspace.
+export ECLAIR_DATA_DIR="${ECLAIR_OUTPUT_DIR}/.data"
+# ECLAIR workspace.
+export ECLAIR_WORKSPACE="${ECLAIR_DATA_DIR}/eclair_workspace"
+
+# Identifies the particular build of the project.
+export ECLAIR_PROJECT_NAME="XEN_${VARIANT}-${SET}"
+# All paths mentioned in ECLAIR reports that are below this directory
+# will be presented as relative to ECLAIR_PROJECT_ROOT.
+export ECLAIR_PROJECT_ROOT="${PWD}"
+
+# Erase and recreate the output directory and the data directory.
+rm -rf "${ECLAIR_OUTPUT_DIR:?}/*"
+mkdir -p "${ECLAIR_DATA_DIR}"
+
+# Perform the build (from scratch) in an ECLAIR environment.
+"${ECLAIR_BIN_DIR}eclair_env" \
+    "-config_file='${SCRIPT_DIR}/analysis.ecl'" \
+    "${EXTRA_ECLAIR_ENV_OPTIONS}" \
+  -- "${SCRIPT_DIR}/../build.sh" "$1" | tee "${ECLAIR_BUILD_LOG}"
+
+
+# Create the project database.
+PROJECT_ECD="${ECLAIR_OUTPUT_DIR}/PROJECT.ecd"
+find "${ECLAIR_DATA_DIR}" -maxdepth 1 -name "FRAME.*.ecb" |
+  sort | xargs cat |
+  "${ECLAIR_BIN_DIR}eclair_report" \
+    "-create_db='${PROJECT_ECD}'" \
+    -load=/dev/stdin > "${ECLAIR_REPORT_LOG}" 2>&1
+
+# Create the Jenkins reports file.
+"${ECLAIR_BIN_DIR}eclair_report" \
+  "-db='${PROJECT_ECD}'" \
+  "-eval_file='${SCRIPT_DIR}/report.ecl'" \
+  >> "${ECLAIR_REPORT_LOG}" 2>&1
+
+"${SCRIPT_DIR}/print_analyzed_files.sh" "${PROJECT_ECD}" "${ECLAIR_OUTPUT_DIR}"
diff --git a/automation/eclair_analysis/ECLAIR/call_properties.ecl b/automation/eclair_analysis/ECLAIR/call_properties.ecl
new file mode 100644
index 0000000000..3f7794bf8b
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/call_properties.ecl
@@ -0,0 +1,106 @@
+
+-call_properties+={"name(printk)", {"pointee_write(1..=never)", "taken()"}}
+-call_properties+={"name(debugtrace_printk)", {"pointee_write(1..=never)", "taken()"}}
+-call_properties+={"name(panic)", {"pointee_write(1..=never)", "taken()"}}
+-call_properties+={"macro(^domain_crash$)", {"pointee_write(2..=never)", "taken()"}}
+-call_properties+={"macro(^(g?d|mm_)?printk$)", {"pointee_write(2..=never)", "taken()"}}
+-call_properties+={"macro(^guest_bug_on_failed$)", {"pointee_write(1=never)", "taken()"}}
+-call_properties+={"macro(^spin_lock_init_prof$)", {"pointee_write(2=never)", "taken()"}}
+-call_properties+={"macro(^sched_test_func$)", {"pointee_write(1..=never)", "taken()"}}
+-call_properties+={"macro(^dev_(info|warn)$)", {"pointee_write(1..=never)", "taken()"}}
+-call_properties+={"macro(^PAGING_DEBUG$)", {"pointee_write(1..=never)", "taken()"}}
+-call_properties+={"macro(^ACPI_(WARNING|ERROR|INFO)$)", {"pointee_write(1..=never)", "taken()"}}
+-call_properties+={"name(fdt_get_property_by_offset_)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
+-call_properties+={"name(read_atomic_size)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
+-call_properties+={"name(device_tree_get_reg)", {"pointee_write(4..=always)", "pointee_read(4..=never)", "taken()"}}
+-call_properties+={"name(dt_get_range)", {"pointee_write(3..=always)", "pointee_read(3..=never)", "taken()"}}
+-call_properties+={"name(parse_static_mem_prop)", {"pointee_write(2..=always)", "pointee_read(2..=never)", "taken()"}}
+-call_properties+={"name(get_ttbr_and_gran_64bit)", {"pointee_write(1..2=always)", "pointee_read(1..2=never)", "taken()"}}
+-call_properties+={"name(hvm_emulate_init_once)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-call_properties+={"name(__vmread)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
+-call_properties+={"name(hvm_pci_decode_addr)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
+-call_properties+={"name(vpci_mmcfg_decode_addr)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
+-call_properties+={"name(x86emul_decode)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-call_properties+={"name(unmap_grant_ref)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
+-call_properties+={"name(arm_smmu_cmdq_build_cmd)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-call_properties+={"name(pci_size_mem_bar)", {"pointee_write(4=always)", "pointee_read(4=never)", "taken()"}}
+-call_properties+={"name(_hvm_read_entry)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
+-call_properties+={"name(hvm_map_guest_frame_rw)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
+-call_properties+={"name(guest_cpuid)", {"pointee_write(4=always)", "pointee_read(4=never)", "taken()"}}
+-call_properties+={"name(epte_get_entry_emt)", {"pointee_write(5=always)", "pointee_read(5=never)", "taken()"}}
+-call_properties+={"name(mcheck_mca_logout)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
+-call_properties+={"name(set_field_in_reg_u32)", {"pointee_write(5=always)", "pointee_read(5=never)", "taken()"}}
+-call_properties+={"name(alloc_affinity_masks)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-call_properties+={"name(xasprintf)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-call_properties+={"name(find_non_smt)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
+-call_properties+={"name(call_rcu)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-call_properties+={"name(getdomaininfo)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
+-call_properties+={"^MAPPING_(INSERT|SEARCH)\\(.*$", {"pointee_write(2..=always)", "pointee_read(2..=never)", "taken()"}}
+-call_properties+={"name(FormatDec)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
+-call_properties+={"name(FormatHex)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
+-call_properties+={"name(p2m_get_ioreq_server)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
+-call_properties+={"name(elf_memset_unchecked)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-call_properties+={"name(set_iommu_pte_present)", {"pointee_write(7=always)", "pointee_read(7=never)", "taken()"}}
+-call_properties+={"name(clear_iommu_pte_present)", {"pointee_write(4=always)", "pointee_read(4=never)", "taken()"}}
+-call_properties+={"name(vcpu_runstate_get)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
+-call_properties+={"name(va_start)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-call_properties+={"name(sgi_target_init)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-call_properties+={"name(get_hw_residencies)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
+-call_properties+={"name(x86_cpu_policy_to_featureset)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
+-call_properties+={"^simple_strtou?ll?\\(.*$", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
+-call_properties+={"name(msi_compose_msg)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
+-call_properties+={"name(print_tainted)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-call_properties+={"name(get_hvm_registers)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
+-call_properties+={"name(x86_insn_modrm)", {"pointee_write(2..3=always)", "pointee_read(2..3=never)", "taken()"}}
+-call_properties+={"name(cpuid_count_leaf)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
+-call_properties+={"name(rcu_lock_remote_domain_by_id)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
+-call_properties+={"name(cpuid_count)", {"pointee_write(3..=always)", "pointee_read(3..=never)", "taken()"}}
+-call_properties+={"name(efi_boot_mem_unused)", {"pointee_write(1..=always)", "pointee_read(1..=never)", "taken()"}}
+-call_properties+={"name(collect_time_info)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
+-call_properties+={"name(setup_xstate_comp)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-call_properties+={"name(map_domain_gfn)", {"pointee_read(5=never)", "taken()"}}
+-call_properties+={"name(fdt_getprop)", {"pointee_read(4=never)", "taken()"}}
+-call_properties+={"name(fdt_get_name)", {"pointee_read(3=never)", "taken()"}}
+-call_properties+={"name(fdt_get_property)", {"pointee_read(4=never)", "taken()"}}
+-call_properties+={"name(pci_get_host_bridge_segment)", {"pointee_read(2=never)", "taken()"}}
+-call_properties+={"name(dt_get_property)", {"pointee_read(3=never)", "taken()"}}
+-call_properties+={"name(dt_property_read_u32)", {"pointee_read(3=never)", "taken()"}}
+-call_properties+={"name(dt_device_get_paddr)", {"pointee_read(3..4=never)", "taken()"}}
+-call_properties+={"name(get_evtchn_dt_property)", {"pointee_write(2..3=maybe)", "pointee_read(2..3=never)", "taken()"}}
+-call_properties+={"name(setup_chosen_node)", {"pointee_write(2..3=maybe)", "pointee_read(2..3=never)", "taken()"}}
+-call_properties+={"name(queue_remove_raw)", {"pointee_read(2=never)", "taken()"}}
+-call_properties+={"macro(^memset$)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-call_properties+={"macro(^va_start$)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-call_properties+={"macro(^memcmp$)", {"pointee_write(1..2=never)", "taken()"}}
+-call_properties+={"macro(^memcpy$)", {"pointee_write(1=always&&2..=never)", "pointee_read(1=never&&2..=always)", "taken()"}}
+
+-doc_begin="Property inferred as a consequence of the semantics of device_tree_get_reg"
+-call_properties+={"name(acquire_static_memory_bank)", {"pointee_write(4..=always)", "pointee_read(4..=never)", "taken()"}}
+-doc_end
+
+-doc_begin="Property inferred as a consequence of the semantics of dt_set_cell"
+-call_properties+={"name(set_interrupt)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-doc_end
+
+-doc_begin="Property inferred as a consequence of the semantics of __p2m_get_mem_access"
+-call_properties+={"name(p2m_get_mem_access)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
+-doc_end
+
+-doc_begin="This function has alternative definitions with props {write=always,read=never} and {write=never,read=never}"
+-call_properties+={"name(alloc_cpumask_var)", {"pointee_write(1=maybe)", "pointee_read(1=never)", "taken()"}}
+-doc_end
+
+-doc_begin="Property inferred as a consequence of the semantics of alloc_cpumask_var"
+-call_properties+={"name(xenctl_bitmap_to_cpumask)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-doc_end
+
+-doc_begin="The call to bitmap_and causes the pointee of dstp to be always written"
+-call_properties+={"^cpumask_(and|andnot|clear|copy|complement).*$", {"pointee_write(1=always)", "pointee_read(1=never)" "taken()"}}
+-call_properties+={"^bitmap_(andnot|complement|fill).*$", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-doc_end
+
+-doc_begin="The .*copy_(to|from).* helpers all have a memcpy-like expectation that the destination is a copy of the source.
+Furthermore, their uses do initialize the involved variables as needed by futher uses in the caller."
+-call_properties+={"macro(^(__)?(raw_)?copy_from_(paddr|guest|compat)(_offset)?$)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
+-call_properties+={"macro(^(__)?copy_to_(guest|compat)(_offset)?$)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
+-doc_end
diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/automation/eclair_analysis/ECLAIR/deviations.ecl
new file mode 100644
index 0000000000..e1a06daf2f
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
@@ -0,0 +1,298 @@
+### Set 1 ###
+
+#
+# Series 2.
+#
+
+-doc_begin="The compiler implementation guarantees that the unreachable code is removed.
+Constant expressions and unreachable branches of if and switch statements are expected."
+-config=MC3R1.R2.1,+reports={safe,"first_area(^.*has an invariantly.*$)"}
+-config=MC3R1.R2.1,+reports={safe,"first_area(^.*incompatible with labeled statement$)"}
+-doc_end
+
+-doc_begin="Some functions are intended to be not referenced."
+-config=MC3R1.R2.1,+reports={deliberate,"first_area(^.*is never referenced$)"}
+-doc_end
+
+-doc_begin="Unreachability in the following macros are expected and safe."
+-config=MC3R1.R2.1,statements+={safe,"macro(name(BUG||assert_failed||ERROR_EXIT||ERROR_EXIT_DOM||PIN_FAIL))"}
+-doc_end
+
+-doc_begin="Proving compliance with respect to Rule 2.2 is generally impossible:
+see https://arxiv.org/abs/2212.13933 for details. Moreover, peer review gives us
+confidence that no evidence of errors in the program's logic has been missed due
+to undetected violations of Rule 2.2, if any. Testing on time behavior gives us
+confidence on the fact that, should the program contain dead code that is not
+removed by the compiler, the resulting slowdown is negligible."
+-config=MC3R1.R2.2,reports+={disapplied,"any()"}
+-doc_end
+
+#
+# Series 3.
+#
+
+-doc_begin="Comments starting with '/*' and containing hyperlinks are safe as
+they are not instances of commented-out code."
+-config=MC3R1.R3.1,reports+={safe, "first_area(text(^.*https?://.*$))"}
+-doc_end
+
+#
+# Series 4.
+#
+
+-doc_begin="The directive has been accepted only for the ARM codebase."
+-config=MC3R1.D4.3,reports+={disapplied,"!(any_area(any_loc(file(^xen/arch/arm/arm64/.*$))))"}
+-doc_end
+
+-doc_begin="Depending on the compiler, rewriting the following function-like
+macros as inline functions is not guaranteed to have the same effect."
+-config=MC3R1.D4.9,macros+={deliberate,"name(likely)"}
+-config=MC3R1.D4.9,macros+={deliberate,"name(unlikely)"}
+-config=MC3R1.D4.9,macros+={deliberate,"name(unreachable)"}
+-doc_end
+
+-doc_begin="These macros can be used on both pointers and unsigned long type values."
+-config=MC3R1.D4.9,macros+={safe,"name(virt_to_maddr)"}
+-config=MC3R1.D4.9,macros+={safe,"name(virt_to_mfn)"}
+-doc_end
+
+-doc_begin="Rewriting variadic macros as variadic functions might have a negative impact on safety."
+-config=MC3R1.D4.9,macros+={deliberate,"variadic()"}
+-doc_end
+
+-doc_begin="Rewriting macros with arguments that are, in turn, arguments of
+__builtin_constant_p() can change the behavior depending on the optimization
+level."
+-config=MC3R1.D4.9,macro_argument_context+="skip_to(class(type||expr||decl,any),
+                                            call(name(__builtin_constant_p)))"
+-doc_end
+
+-doc_begin="Function-like macros defined in public headers are meant to be
+usable in C89 mode without any extensions. Hence they cannot be replaced by
+inline functions."
+-config=MC3R1.D4.9,macros+={deliberate, "loc(file(api:public))"}
+-doc_end
+
+-doc_begin="This header file is autogenerated or empty, therefore it poses no
+risk if included more than once."
+-file_tag+={empty_header, "^xen/arch/arm/efi/runtime\\.h$"}
+-file_tag+={autogen_headers, "^xen/include/xen/compile\\.h$||^xen/include/generated/autoconf.h$||^xen/include/xen/hypercall-defs.h$"}
+-config=MC3R1.D4.10,reports+={safe, "all_area(all_loc(file(empty_header||autogen_headers)))"}
+-doc_end
+
+-doc_begin="Files that are intended to be included more than once do not need to
+conform to the directive."
+-config=MC3R1.D4.10,reports+={safe, "first_area(text(^/\\* This file is legitimately included multiple times\\. \\*/$, begin-4))"}
+-config=MC3R1.D4.10,reports+={safe, "first_area(text(^/\\* Generated file, do not edit! \\*/$, begin-3))"}
+-doc_end
+
+#
+# Series 5.
+#
+
+-doc_begin="The project adopted the rule with an exception listed in
+'docs/misra/rules.rst'"
+-config=MC3R1.R5.3,reports+={safe, "any_area(any_loc(any_exp(macro(^READ_SYSREG$))&&any_exp(macro(^WRITE_SYSREG$))))"}
+-config=MC3R1.R5.3,reports+={safe, "any_area(any_loc(any_exp(macro(^max_t$))&&any_exp(macro(^min_t$))))"}
+-config=MC3R1.R5.3,reports+={safe, "any_area(any_loc(any_exp(macro(^read[bwlq]$))&&any_exp(macro(^read[bwlq]_relaxed$))))"}
+-config=MC3R1.R5.3,reports+={safe, "any_area(any_loc(any_exp(macro(^per_cpu$))&&any_exp(macro(^this_cpu$))))"}
+-doc_end
+
+-doc_begin="The identifier 'fdt' is a widely-used name, for which no suitable
+substitute can be found. It is understood in 'xen/arch/arm/efi-boot.h' that the
+static variable 'fdt' cannot be confused with parameter names of the function
+declarations that are present in the file."
+-file_tag+={efi_boot_h, "^xen/arch/arm/efi/efi-boot\\.h$"}
+-config=MC3R1.R5.3,reports+={deliberate, "any_area(decl(kind(var)&&static_storage()&&^fdt$)&&any_loc(file(efi_boot_h)))"}
+-doc_end
+
+-doc_begin="The identifier 'start' is a widely-used name, for which no suitable
+substitute can be found. It is understood in 'xen/include/xen/kernel.h' that the
+extern variable 'start' cannot be confused with omonymous parameter names of the
+function declarations where that variable is visible."
+-file_tag+={kernel_h, "^xen/include/xen/kernel\\.h$"}
+-config=MC3R1.R5.3,reports+={deliberate, "any_area(decl(kind(var)&&linkage(external)&&^start$)&&any_loc(file(kernel_h)))"}
+-doc_end
+
+-doc_begin="Function-like macros cannot be confused with identifiers that are
+neither functions nor pointers to functions."
+-config=MC3R1.R5.5,reports={safe,"all_area(decl(node(enum_decl||record_decl||field_decl||param_decl||var_decl)&&!type(canonical(address((node(function||function_no_proto))))))||macro(function_like()))"}
+-doc_end
+
+-doc_begin="The use of these identifiers for both macro names and other entities
+is deliberate and does not generate developer confusion."
+-config=MC3R1.R5.5,reports+={safe, "any_area(text(^\\s*/\\*\\s+SAF-[0-9]+-safe\\s+MC3R1\\.R5\\.5.*$, begin-1))"}
+-doc_end
+
+-doc_begin="The definition of macros and functions ending in '_bit' that use the
+same identifier in 'bitops.h' is deliberate and safe."
+-file_tag+={bitops_h, "^xen/arch/x86/include/asm/bitops\\.h$"}
+-config=MC3R1.R5.5,reports+={safe, "all_area((decl(^.*_bit\\(.*$)||macro(^.*_bit$))&&all_loc(file(bitops_h)))"}
+-doc_end
+
+-doc_begin="The definition of macros and functions beginning in 'str' or 'mem'
+that use the same identifier in 'xen/include/xen/string.h' is deliberate and
+safe."
+-file_tag+={string_h, "^xen/include/xen/string\\.h$"}
+-config=MC3R1.R5.5,reports+={safe, "any_area((decl(^(mem|str).*$)||macro(^(mem|str).*$))&&all_loc(file(string_h)))"}
+-doc_end
+
+#
+# Series 7.
+#
+
+-doc_begin="Usage of the following constants is safe, since they are given as-is
+in the inflate algorithm specification and there is therefore no risk of them
+being interpreted as decimal constants."
+-config=MC3R1.R7.1,literals={safe, "^0(007|37|070|213|236|300|321|330|331|332|333|334|335|337|371)$"}
+-doc_end
+
+-doc_begin="Violations in files that maintainers have asked to not modify in the
+context of R7.2."
+-file_tag+={adopted_r7_2,"^xen/include/xen/libfdt/.*$"}
+-file_tag+={adopted_r7_2,"^xen/arch/x86/include/asm/x86_64/efibind.h$"}
+-file_tag+={adopted_r7_2,"^xen/include/efi/efiapi\\.h$"}
+-file_tag+={adopted_r7_2,"^xen/include/efi/efidef\\.h$"}
+-file_tag+={adopted_r7_2,"^xen/include/efi/efiprot\\.h$"}
+-file_tag+={adopted_r7_2,"^xen/arch/x86/cpu/intel\\.c$"}
+-file_tag+={adopted_r7_2,"^xen/arch/x86/cpu/amd\\.c$"}
+-file_tag+={adopted_r7_2,"^xen/arch/x86/cpu/common\\.c$"}
+-config=MC3R1.R7.2,reports+={deliberate,"any_area(any_loc(file(adopted_r7_2)))"}
+-doc_end
+
+-doc_begin="Violations caused by __HYPERVISOR_VIRT_START are related to the
+particular use of it done in xen_mk_ulong."
+-config=MC3R1.R7.2,reports+={deliberate,"any_area(any_loc(macro(name(BUILD_BUG_ON))))"}
+-doc_end
+
+-doc_begin="The following string literals are assigned to pointers to non
+const-qualified char."
+-config=MC3R1.R7.4,reports+={safe, "any_area(text(^\\s*/\\*\\s+SAF-[0-9]+-safe\\s+MC3R1\\.R7\\.4.*$, begin-1))"}
+-doc_end
+
+-doc_begin="Allow pointers of non-character type as long as the pointee is
+const-qualified."
+-config=MC3R1.R7.4,same_pointee=false
+-doc_end
+
+#
+# Series 8.
+#
+
+-doc_begin="The following variables are compiled in multiple translation units
+belonging to different executables and therefore are safe."
+-config=MC3R1.R8.6,declarations+={safe, "name(current_stack_pointer||bsearch||sort)"}
+-doc_end
+
+-doc_begin="Declarations without definitions are allowed (specifically when the
+definition is compiled-out or optimized-out by the compiler)"
+-config=MC3R1.R8.6,reports+={deliberate, "first_area(^.*has no definition$)"}
+-doc_end
+
+-doc_begin="The gnu_inline attribute without static is deliberately allowed."
+-config=MC3R1.R8.10,declarations+={deliberate,"property(gnu_inline)"}
+-doc_end
+
+#
+# Series 9.
+#
+
+-doc_begin="The following variables are written before being set, therefore no
+access to uninitialized memory locations happens, as explained in the deviation
+comment."
+-config=MC3R1.R9.1,reports+={safe, "any_area(text(^\\s*/\\*\\s+SAF-[0-9]+-safe\\s+MC3R1\\.R9\\.1.*$, begin-1))"}
+-doc_end
+
+-doc_begin="Violations in files that maintainers have asked to not modify in the
+context of R9.1."
+-file_tag+={adopted_r9_1,"^xen/arch/arm/arm64/lib/find_next_bit\\.c$"}
+-config=MC3R1.R9.1,reports+={deliberate,"any_area(any_loc(file(adopted_r9_1)))"}
+-doc_end
+
+-doc_begin="The possibility of committing mistakes by specifying an explicit
+dimension is higher than omitting the dimension."
+-config=MC3R1.R9.5,reports+={deliberate, "any()"}
+-doc_end
+
+### Set 2 ###
+
+#
+# Series 10.
+#
+
+-doc_begin="The value-preserving conversions of integer constants are safe"
+-config=MC3R1.R10.1,etypes={safe,"any()","preserved_integer_constant()"}
+-config=MC3R1.R10.3,etypes={safe,"any()","preserved_integer_constant()"}
+-config=MC3R1.R10.4,etypes={safe,"any()","preserved_integer_constant()||sibling(rhs,preserved_integer_constant())"}
+-doc_end
+
+-doc_begin="Shifting non-negative integers to the right is safe."
+-config=MC3R1.R10.1,etypes+={safe,
+  "stmt(node(binary_operator)&&operator(shr))",
+  "src_expr(definitely_in(0..))"}
+-doc_end
+
+-doc_begin="Shifting non-negative integers to the left is safe if the result is
+still non-negative."
+-config=MC3R1.R10.1,etypes+={safe,
+  "stmt(node(binary_operator)&&operator(shl)&&definitely_in(0..))",
+  "src_expr(definitely_in(0..))"}
+-doc_end
+
+-doc_begin="Bitwise logical operations on non-negative integers are safe."
+-config=MC3R1.R10.1,etypes+={safe,
+  "stmt(node(binary_operator)&&operator(and||or||xor))",
+  "src_expr(definitely_in(0..))"}
+-doc_end
+
+-doc_begin="The implicit conversion to Boolean for logical operator arguments is well known to all Xen developers to be a comparison with 0"
+-config=MC3R1.R10.1,etypes+={safe, "stmt(operator(logical)||node(conditional_operator||binary_conditional_operator))", "dst_type(ebool||boolean)"}
+-doc_end
+
+### Set 3 ###
+
+#
+# Series 18.
+#
+
+-doc_begin="FIXME: explain why pointer differences involving this macro are safe."
+-config=MC3R1.R18.2,reports+={safe,"all_area(all_loc(any_exp(macro(^ACPI_PTR_DIFF$))))"}
+-doc_end
+
+-doc_begin="FIXME: explain why pointer differences involving this macro are safe."
+-config=MC3R1.R18.2,reports+={safe,"all_area(all_loc(any_exp(macro(^page_to_mfn$))))"}
+-doc_end
+
+-doc_begin="FIXME: explain why pointer differences involving this macro are safe."
+-config=MC3R1.R18.2,reports+={safe,"all_area(all_loc(any_exp(macro(^page_to_pdx$))))"}
+-doc_end
+
+#
+# Series 20.
+#
+
+-doc_begin="Code violating Rule 20.7 is safe when macro parameters are used: (1)
+as function arguments; (2) as macro arguments; (3) as array indices; (4) as lhs
+in assignments."
+-config=MC3R1.R20.7,expansion_context=
+{safe, "context(__call_expr_arg_contexts)"},
+{safe, "context(skip_to(__expr_non_syntactic_contexts, stmt_child(node(array_subscript_expr), subscript)))"},
+{safe, "context(skip_to(__expr_non_syntactic_contexts, stmt_child(operator(assign), lhs)))"},
+{safe, "left_right(^[(,\\[]$,^[),\\]]$)"}
+-doc_end
+
+#
+# Developer confusion
+#
+
+-doc="Selection for reports that are fully contained in adopted code."
+-report_selector+={adopted_report,"all_area(!kind(culprit||evidence)||all_loc(all_exp(adopted||pseudo)))"}
+
+-doc_begin="Adopted code is not meant to be read, reviewed or modified by human
+programmers:no developers' confusion is not possible. In addition, adopted code
+is assumed to work as is. Reports that are fully contained in adopted code are
+hidden/tagged with the 'adopted' tag."
+-service_selector={developer_confusion_guidelines,"^(MC3R1\\.R2\\.1|MC3R1\\.R2\\.2|MC3R1\\.R2\\.3|MC3R1\\.R2\\.4|MC3R1\\.R2\\.5|MC3R1\\.R2\\.6|MC3R1\\.R2\\.7|MC3R1\\.R4\\.1|MC3R1\\.R5\\.3|MC3R1\\.R5\\.6|MC3R1\\.R5\\.7|MC3R1\\.R5\\.8|MC3R1\\.R5\\.9|MC3R1\\.R7\\.1|MC3R1\\.R7\\.2|MC3R1\\.R7\\.3|MC3R1\\.R8\\.7|MC3R1\\.R8\\.8|MC3R1\\.R8\\.9|MC3R1\\.R8\\.11|MC3R1\\.R8\\.12|MC3R1\\.R8\\.13|MC3R1\\.R9\\.3|MC3R1\\.R9\\.4|MC3R1\\.R9\\.5|MC3R1\\.R10\\.2|MC3R1\\.R10\\.5|MC3R1\\.R10\\.6|MC3R1\\.R10\\.7|MC3R1\\.R10\\.8|MC3R1\\.R11\\.9|MC3R1\\.R12\\.1|MC3R1\\.R12\\.3|MC3R1\\.R12\\.4|MC3R1\\.R13\\.5|MC3R1\\.R14\\.1|MC3R1\\.R14\\.2|MC3R1\\.R14\\.3|MC3R1\\.R15\\.1|MC3R1\\.R15\\.2|MC3R1\\.R15\\.3|MC3R1\\.R15\\.4|MC3R1\\.R15\\.5|MC3R1\\.R15\\.6|MC3R1\\.R15\\.7|MC3R1\\.R16\\.1|MC3R1\\.R16\\.2|MC3R1\\.R16\\.3|MC3R1\\.R16\\.4|MC3R1\\.R16\\.5|MC3R1\\.R16\\.6|MC3R1\\.R16\\.7|MC3R1\\.R17\\.7|MC3R1\\.R17\\.8|MC3R1\\.R18\\.4|MC3R1\\.R18\\.5)$"
+}
+-config=developer_confusion_guidelines,reports+={relied,adopted_report}
+-doc_end
diff --git a/automation/eclair_analysis/ECLAIR/out_of_scope.ecl b/automation/eclair_analysis/ECLAIR/out_of_scope.ecl
new file mode 100644
index 0000000000..44db6997b5
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/out_of_scope.ecl
@@ -0,0 +1,127 @@
+-doc_begin="Imported from Linux: ignore for now."
+-file_tag+={adopted,"^xen/common/libfdt/.*$"}
+-file_tag+={adopted,"^xen/include/xen/libfdt/.*$"}
+-file_tag+={adopted,"^xen/common/xz/.*$"}
+-file_tag+={adopted,"^xen/common/zstd/.*$"}
+-file_tag+={adopted,"^xen/drivers/acpi/apei/.*$"}
+-file_tag+={adopted,"^xen/drivers/acpi/tables/.*$"}
+-file_tag+={adopted,"^xen/drivers/acpi/utilities/.*$"}
+-file_tag+={adopted,"^xen/drivers/video/font_.*$"}
+-file_tag+={adopted,"^xen/arch/arm/arm64/cpufeature\\.c$"}
+-file_tag+={adopted,"^xen/arch/arm/arm64/insn\\.c$"}
+-file_tag+={adopted,"^xen/arch/arm/arm64/lib/find_next_bit\\.c$"}
+-file_tag+={adopted,"^xen/common/bitmap\\.c$"}
+-file_tag+={adopted,"^xen/common/bunzip2\\.c$"}
+-file_tag+={adopted,"^xen/common/earlycpio\\.c$"}
+-file_tag+={adopted,"^xen/common/inflate\\.c$"}
+-file_tag+={adopted,"^xen/common/lzo\\.c$"}
+-file_tag+={adopted,"^xen/common/lz4/decompress\\.c$"}
+-file_tag+={adopted,"^xen/common/radix-tree\\.c$"}
+-file_tag+={adopted,"^xen/common/ubsan/ubsan\\.c$"}
+-file_tag+={adopted,"^xen/drivers/acpi/hwregs\\.c$"}
+-file_tag+={adopted,"^xen/drivers/acpi/numa\\.c$"}
+-file_tag+={adopted,"^xen/drivers/acpi/osl\\.c$"}
+-file_tag+={adopted,"^xen/drivers/acpi/tables\\.c$"}
+-file_tag+={adopted,"^xen/lib/list-sort\\.c$"}
+-file_tag+={adopted,"^xen/lib/rbtree\\.c$"}
+-file_tag+={adopted,"^xen/lib/xxhash.*\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/acpi/boot\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/acpi/cpu_idle\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/acpi/cpufreq/cpufreq\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/acpi/cpuidle_menu\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/acpi/lib\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/cpu/amd\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/cpu/centaur\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/cpu/common\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/cpu/hygon\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/cpu/intel\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/cpu/intel_cacheinfo\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/cpu/mcheck/non-fatal\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/cpu/mtrr/.*$"}
+-file_tag+={adopted,"^xen/arch/x86/cpu/mwait-idle\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/delay\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/dmi_scan\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/mpparse\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/srat\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/time\\.c$"}
+-file_tag+={adopted,"^xen/arch/x86/x86_64/mmconf-fam10h\\.c$"}
+-doc_end
+
+-doc_begin="Intel specific source files are out of scope."
+-file_tag+={out_of_scope,"^xen/arch/x86/cpu/intel\\.c$"}
+-file_tag+={out_of_scope,"^xen/arch/x86/cpu/intel_cacheinfo\\.c$"}
+-file_tag+={out_of_scope,"^xen/arch/x86/cpu/microcode/intel\\.c$"}
+-file_tag+={out_of_scope,"^xen/arch/x86/cpu/shanghai\\.c$"}
+-file_tag+={out_of_scope,"^xen/arch/x86/hvm/vmx/.*$"}
+-file_tag+={out_of_scope,"^xen/arch/x86/include/asm/hvm/vmx/.*$"}
+-file_tag+={out_of_scope,"^xen/drivers/passthrough/vtd/.*$"}
+-file_tag+={out_of_scope,"^xen/arch/x86/cpu/mcheck/mce_intel\\.c$"}
+-file_tag+={out_of_scope,"^xen/arch/x86/cpu/mwait-idle\\.c$"}
+-file_tag+={out_of_scope,"^xen/arch/x86/cpu/vpmu_intel\\.c$"}
+-file_tag+={out_of_scope,"^xen/arch/x86/tsx\\.c$"}
+-file_tag+={out_of_scope,"^xen/arch/x86/mm/altp2m\\.c$"}
+-file_tag+={out_of_scope,"^xen/arch/x86/mm/p2m-ept\\.c$"}
+-file_tag+={out_of_scope,"^xen/arch/x86/mm/hap/nested_ept\\.c$"}
+-file_tag+={out_of_scope,"^xen/arch/x86/include/asm/altp2m\\.h$"}
+-file_tag+={out_of_scope,"^xen/arch/x86/include/asm/intel-family\\.h$"}
+-doc_end
+
+-doc_begin="Not in scope initially as it generates many violations and it is not enabled in safety configurations."
+-file_tag+={adopted,"^xen/xsm/flask/.*$"}
+-doc_end
+
+-doc_begin="unlz4.c implementation by Yann Collet, the others un* are from Linux, ignore for now."
+-file_tag+={adopted,"^xen/common/un.*\\.c$"}
+-doc_end
+
+-doc_begin="Origin is external and documented in xen/crypto/README.source ."
+-file_tag+={adopted,"^xen/crypto/.*$"}
+-doc_end
+
+-doc_begin="Files imported from the gnu-efi package"
+-file_tag+={adopted,"^xen/include/efi/.*$"}
+-file_tag+={adopted,"^xen/arch/x86/include/asm/x86_64/efibind\\.h$"}
+-doc_end
+
+-doc_begin="Build tools are out of scope."
+-file_tag+={out_of_scope_tools,"^xen/tools/.*$"}
+-file_tag+={out_of_scope_tools,"^xen/arch/x86/efi/mkreloc\\.c$"}
+-file_tag+={out_of_scope_tools,"^xen/arch/x86/boot/mkelf32\\.c$"}
+-doc_end
+
+-doc_begin="Out of scope headers."
+-file_tag+={out_of_scope,"^xen/include/xen/bitmap\\.h$"}
+-file_tag+={out_of_scope,"^xen/include/xen/earlycpio\\.h$"}
+-file_tag+={out_of_scope,"^xen/include/xen/lzo\\.h$"}
+-file_tag+={out_of_scope,"^xen/include/xen/lz4\\.h$"}
+-file_tag+={out_of_scope,"^xen/common/lz4/defs\\.h$"}
+-file_tag+={out_of_scope,"^xen/include/xen/radix-tree\\.h$"}
+-file_tag+={out_of_scope,"^xen/include/xen/list_sort\\.h$"}
+-file_tag+={out_of_scope,"^xen/include/xen/rbtree\\.h$"}
+-file_tag+={out_of_scope,"^xen/include/xen/xxhash\\.h$"}
+-doc_end
+
+-doc_begin="Headers under xen/include/public/ are the description of the public
+hypercall ABI so the community is extremely conservative in making changes
+there, because the interface is maintained for backward compatibility: ignore
+for now."
+-file_tag+={hypercall_ABI, "^xen/include/public/.*$"}
+-source_files+={hide, hypercall_ABI}
+-doc_end
+
+-doc_begin="Consider out-of-scope files external to the project."
+-file_tag+={external, out_of_scope}
+-doc_end
+
+-doc_begin="Consider adopted files external to the project."
+-file_tag+={external, adopted}
+-doc_end
+
+-doc_begin="Disregard out-of-scope tools."
+-frames+={hide,"main(out_of_scope_tools)"}
+-doc_end
+
+-doc_begin="The build performs speculative calls with target /dev/null: this
+frames should be ignored."
+-frames+={hide,"target(^/dev/null$)"}
+-doc_end
diff --git a/automation/eclair_analysis/ECLAIR/print_analyzed_files.sh b/automation/eclair_analysis/ECLAIR/print_analyzed_files.sh
new file mode 100755
index 0000000000..c19a8ecbd0
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/print_analyzed_files.sh
@@ -0,0 +1,66 @@
+#!/bin/bash
+# Stop immediately if any executed command has exit status different from 0.
+set -eu
+
+script_name="$(basename "$0")"
+script_dir="$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )"
+
+fatal() {
+  echo "${script_name}: $*" >&2
+  exit 1
+}
+
+usage() {
+  fatal "Usage: ${script_name} DATABASE OUT_DIR"
+}
+
+extrapolate_regex() {
+  lookbehind=$1
+  file=$2
+  grep -Po "(?<=${lookbehind}\"\\^).*(?=\\$\")" "${file}" | sed 's/\\\\/\\/'
+}
+
+if [ $# -lt 2 ]; then
+  usage
+fi
+
+DB=$1
+OUT_DIR=$2
+
+files_txt="${OUT_DIR}/files.txt"
+files_c_txt="${OUT_DIR}/files_c.txt"
+files_h_txt="${OUT_DIR}/files_h.txt"
+exclusions_txt="${OUT_DIR}/exclusions.txt"
+
+
+if [[ ! -d "${OUT_DIR}" ]]; then
+  mkdir -p "${OUT_DIR}"
+else
+  rm -f "${files_txt}"
+  rm -f "${files_c_txt}"
+  rm -f "${files_h_txt}"
+  rm -f "${exclusions_txt}"
+fi
+
+# Generating txt report with files
+"${ECLAIR_BIN_DIR}eclair_report" -db="${DB}" -files_txt="${files_txt}"
+
+{
+  # Extracting out of scope code
+  out_of_scope_ecl="${script_dir}/out_of_scope.ecl"
+  extrapolate_regex adopted,             "${out_of_scope_ecl}"
+  extrapolate_regex out_of_scope_tools,  "${out_of_scope_ecl}"
+  extrapolate_regex out_of_scope,        "${out_of_scope_ecl}"
+  extrapolate_regex hypercall_ABI,       "${out_of_scope_ecl}"
+  extrapolate_regex "hide, "             "${out_of_scope_ecl}"
+} >"${exclusions_txt}"
+sort -o "${exclusions_txt}" -u "${exclusions_txt}"
+
+# Removing exclusions from files_txt
+grep -E -v "(object: |/dev/pipe)" "${files_txt}" > "${files_txt}.tmp"
+grep -vf "${exclusions_txt}" "${files_txt}.tmp" > "${files_txt}"
+rm "${files_txt}.tmp"
+# Creating files with only headers
+grep -Ev "(xen.*\.(h\w+|[^h]\w*) |.*ecl)" "${files_txt}" > "${files_h_txt}"
+# Creating files with only c files
+grep -Ev "(xen.*\.(c\w+|[^c]\w*) |.*ecl)" "${files_txt}" > "${files_c_txt}"
diff --git a/automation/eclair_analysis/ECLAIR/public_APIs.ecl b/automation/eclair_analysis/ECLAIR/public_APIs.ecl
new file mode 100644
index 0000000000..9701a295e6
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/public_APIs.ecl
@@ -0,0 +1,6 @@
+# Definition of the public APIs.
+
+-doc="All Xen public headers."
+-file_tag+={api:public,"^xen/include/public/.*\\.h$"}
+
+-public_files+=api:public
diff --git a/automation/eclair_analysis/ECLAIR/report.ecl b/automation/eclair_analysis/ECLAIR/report.ecl
new file mode 100644
index 0000000000..6ee324746c
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/report.ecl
@@ -0,0 +1,4 @@
+# eclair_report
+
+reports_codeclimate("gl-code-quality-report.json")
+
diff --git a/automation/eclair_analysis/ECLAIR/tagging.ecl b/automation/eclair_analysis/ECLAIR/tagging.ecl
new file mode 100644
index 0000000000..ef2e56e186
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/tagging.ecl
@@ -0,0 +1,34 @@
+-doc="Hide reports marked as compliant."
+-remap_rtag={compliant,hide}
+
+-doc="Hide reports marked as safe."
+-remap_rtag={safe,hide}
+
+-doc="Hide reports marked as relied."
+-remap_rtag={relied,hide}
+
+-doc="Hide reports marked as deliberate."
+-remap_rtag={deliberate,hide}
+
+-doc="Hide reports marked as disapplied."
+-remap_rtag={disapplied,hide}
+
+#######################
+# Accepted guidelines #
+#######################
+
+-doc="Accepted guidelines as reported in XEN/docs/misra/rules.rst"
+-service_selector={accepted_guidelines,"^(MC3R1\\.D1\\.1|MC3R1\\.D2\\.1|MC3R1\\.D4\\.3|MC3R1\\.D4\\.7|MC3R1\\.D4\\.10|MC3R1\\.D4\\.11|MC3R1\\.D4\\.14|MC3R1\\.R1\\.1|MC3R1\\.R1\\.3|MC3R1\\.R1\\.4|MC3R1\\.R2\\.1|MC3R1\\.R2\\.6|MC3R1\\.R2\\.2|MC3R1\\.R3\\.1|MC3R1\\.R3\\.2|MC3R1\\.R4\\.1|MC3R1\\.R4\\.2|MC3R1\\.R5\\.1|MC3R1\\.R5\\.2|MC3R1\\.R5\\.3|MC3R1\\.R5\\.4|MC3R1\\.R5\\.6|MC3R1\\.R6\\.1|MC3R1\\.R6\\.2|MC3R1\\.R7\\.1|MC3R1\\.R7\\.2|MC3R1\\.R7\\.3|MC3R1\\.R7\\.4|MC3R1\\.R8\\.1|MC3R1\\.R8\\.2|MC3R1\\.R8\\.3|MC3R1\\.R8\\.4|MC3R1\\.R8\\.5|MC3R1\\.R8\\.6|MC3R1\\.R8\\.8|MC3R1\\.R8\\.10|MC3R1\\.R8\\.12|MC3R1\\.R8\\.14|MC3R1\\.R9\\.1|MC3R1\\.R9\\.2|MC3R1\\.R9\\.3|MC3R1\\.R9\\.4|MC3R1\\.R9\\.5|MC3R1\\.R12\\.5|MC3R1\\.R13\\.6|MC3R1\\.R13\\.1|MC3R1\\.R14\\.1|MC3R1\\.R16\\.7|MC3R1\\.R17\\.3|MC3R1\\.R17\\.4|MC3R1\\.R17\\.6|MC3R1\\.R18\\.3|MC3R1\\.R19\\.1|MC3R1\\.R20\\.7|MC3R1\\.R20\\.13|MC3R1\\.R20\\.14|MC3R1\\.R21\\.13|MC3R1\\.R21\\.17|MC3R1\\.R21\\.18|MC3R1\\.R21\\.19|MC3R1\\.R21\\.20|MC3R1\\.R21\\.21|MC3R1\\.R22\\.2|MC3R1\\.R22\\.4|MC3R1\\.R22\\.5|MC3R1\\.R22\\.6)$"
+}
+-doc="All reports of accepted guidelines are tagged as accepted."
+-reports+={status:accepted,"service(accepted_guidelines)"}
+
+####################
+# Clean guidelines #
+####################
+
+-doc_begin="Clean guidelines: new violations for these guidelines are not accepted."
+-service_selector={clean_guidelines,"^(MC3R1\\.D1\\.1|MC3R1\\.D2\\.1|MC3R1\\.D4\\.11|MC3R1\\.D4\\.14|MC3R1\\.R1\\.4|MC3R1\\.R2\\.2|MC3R1\\.R3\\.2|MC3R1\\.R5\\.1|MC3R1\\.R5\\.2|MC3R1\\.R5\\.4|MC3R1\\.R6\\.1|MC3R1\\.R6\\.2|MC3R1\\.R7\\.1|MC3R1\\.R8\\.1|MC3R1\\.R8\\.5|MC3R1\\.R8\\.8|MC3R1\\.R8\\.10|MC3R1\\.R8\\.12|MC3R1\\.R8\\.14|MC3R1\\.R9\\.2|MC3R1\\.R9\\.4|MC3R1\\.R9\\.5|MC3R1\\.R12\\.5|MC3R1\\.R17\\.3|MC3R1\\.R17\\.6|MC3R1\\.R21\\.13|MC3R1\\.R21\\.19|MC3R1\\.R21\\.21|MC3R1\\.R22\\.2|MC3R1\\.R22\\.4|MC3R1\\.R22\\.5)$"
+}
+-reports+={clean:added,"service(clean_guidelines)"}
+-doc_end
diff --git a/automation/eclair_analysis/ECLAIR/toolchain.ecl b/automation/eclair_analysis/ECLAIR/toolchain.ecl
new file mode 100644
index 0000000000..e6cd289b5e
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/toolchain.ecl
@@ -0,0 +1,275 @@
+# Compilers.
+-file_tag+={GCC_ARM64,"^/usr/bin/aarch64-linux-gnu-gcc-12$"}
+-file_tag+={GCC_X86_64,"^/usr/bin/x86_64-linux-gnu-gcc-12$"}
+
+# Manuals.
+-setq=GCC_MANUAL,"https://gcc.gnu.org/onlinedocs/gcc-12.1.0/gcc.pdf"
+-setq=CPP_MANUAL,"https://gcc.gnu.org/onlinedocs/gcc-12.1.0/cpp.pdf"
+-setq=ARM64_ABI_MANUAL,"https://github.com/ARM-software/abi-aa/blob/60a8eb8c55e999d74dac5e368fc9d7e36e38dda4/aapcs64/aapcs64.rst"
+-setq=X86_64_ABI_MANUAL,"https://gitlab.com/x86-psABIs/x86-64-ABI/-/jobs/artifacts/master/raw/x86-64-ABI/abi.pdf?job=build"
+-setq=ARM64_LIBC_MANUAL,"https://www.gnu.org/software/libc/manual/pdf/libc.pdf"
+-setq=X86_64_LIBC_MANUAL,"https://www.gnu.org/software/libc/manual/pdf/libc.pdf"
+-setq=C99_STD,"ISO/IEC 9899:1999"
+
+-doc_begin="
+    _Static_assert: see Section \"2.1 C Language\" of "GCC_MANUAL".
+    asm, __asm__: see Sections \"6.48 Alternate Keywords\" and \"6.47 How to Use Inline Assembly Language in C Code\" of "GCC_MANUAL".
+    __volatile__: see Sections \"6.48 Alternate Keywords\" and \"6.47.2.1 Volatile\" of "GCC_MANUAL".
+    __const__, __inline__, __inline: see Section \"6.48 Alternate Keywords\" of "GCC_MANUAL".
+    typeof, __typeof__: see Section \"6.7 Referring to a Type with typeof\" of "GCC_MANUAL".
+    __alignof__, __alignof: see Sections \"6.48 Alternate Keywords\" and \"6.44 Determining the Alignment of Functions, Types or Variables\" of "GCC_MANUAL".
+    __attribute__: see Section \"6.39 Attribute Syntax\" of "GCC_MANUAL".
+    __builtin_types_compatible_p: see Section \"6.59 Other Built-in Functions Provided by GCC\" of "GCC_MANUAL".
+    __builtin_va_arg: non-documented GCC extension.
+    __builtin_offsetof: see Section \"6.53 Support for offsetof\" of "GCC_MANUAL".
+"
+-config=STD.tokenext,behavior+={c99, GCC_ARM64, "^(_Static_assert|asm|__asm__|__volatile__|__const__|__inline__|typeof|__typeof__|__alignof__|__attribute__|__builtin_types_compatible_p|__builtin_va_arg|__builtin_offsetof)$"}
+-config=STD.tokenext,behavior+={c99, GCC_X86_64, "^(_Static_assert|asm|__asm__|__volatile__|__const__|__inline__|__inline|typeof|__typeof__|__alignof__|__alignof|__attribute__|__builtin_types_compatible_p|__builtin_va_arg|__builtin_offsetof)$"}
+-doc_end
+
+-doc_begin="Non-documented GCC extension."
+-config=STD.emptinit,behavior+={c99,GCC_ARM64,specified}
+-config=STD.emptinit,behavior+={c99,GCC_X86_64,specified}
+#-config=STD.emptinit,behavior+={c18,GCC_X86_64,specified}
+-doc_end
+
+-doc_begin="See Section \"6.24 Arithmetic on void- and Function-Pointers\" of "GCC_MANUAL"."
+-config=STD.vptrarth,behavior+={c99,GCC_ARM64,specified}
+-config=STD.vptrarth,behavior+={c99,GCC_X86_64,specified}
+-doc_end
+
+-doc_begin="See Section \"6.1 Statements and Declarations in Expressions\" of "GCC_MANUAL"."
+-config=STD.stmtexpr,behavior+={c99,GCC_ARM64,specified}
+-config=STD.stmtexpr,behavior+={c99,GCC_X86_64,specified}
+-doc_end
+
+-doc_begin="See Section \"6.19 Structures with No Members\" of "GCC_MANUAL"."
+-config=STD.emptrecd,behavior+={c99,GCC_ARM64,specified}
+-config=STD.emptrecd,behavior+={c99,GCC_X86_64,specified}
+-doc_end
+
+-doc_begin="See Section \"6.18 Arrays of Length Zero\" of "GCC_MANUAL"."
+-config=STD.arayzero,behavior+={c99,GCC_ARM64,specified}
+-config=STD.arayzero,behavior+={c99,GCC_X86_64,specified}
+-doc_end
+
+-doc_begin="See Section \"6.8 Conditionals with Omitted Operands\" of "GCC_MANUAL"."
+-config=STD.bincondl,behavior+={c99,GCC_ARM64,specified}
+-config=STD.bincondl,behavior+={c99,GCC_X86_64,specified}
+-doc_end
+
+-doc_begin="See Section \"6.30 Case Ranges\" of "GCC_MANUAL"."
+-config=STD.caseuplw,behavior+={c99,GCC_ARM64,specified}
+-config=STD.caseuplw,behavior+={c99,GCC_X86_64,specified}
+-doc_end
+
+-doc_begin="See Section \"6.63 Unnamed Structure and Union Fields\" of "GCC_MANUAL"."
+-config=STD.anonfild,behavior+={c99,GCC_ARM64,specified}
+-config=STD.anonfild,behavior+={c99,GCC_X86_64,specified}
+-doc_end
+
+-doc_begin="Non-documented GCC extension."
+-config=STD.emptdecl,behavior+={c99,GCC_ARM64,specified}
+-config=STD.emptdecl,behavior+={c99,GCC_X86_64,specified}
+-doc_end
+
+-doc_begin="Non-documented GCC extension."
+-config=STD.emptenum,behavior+={c99,GCC_ARM64,specified}
+-doc_end
+
+-doc_begin="Non-documented GCC extension."
+-config=STD.pteincmp,behavior+={c99,GCC_ARM64,specified}
+-config=STD.pteincmp,behavior+={c99,GCC_X86_64,specified}
+#-config=STD.pteincmp,behavior+={c18,GCC_X86_64,specified}
+-doc_end
+
+-doc_begin="Non-documented GCC extension."
+-config=STD.funojptr,behavior+={c99,GCC_X86_64,specified}
+-doc_end
+
+-doc_begin="
+    ext_paste_comma: see Section \"6.21 Macros with a Variable Number of Arguments\" of "GCC_MANUAL".
+    ext_missing_varargs_arg: see Section \"6.21 Macros with a Variable Number of Arguments\" of "GCC_MANUAL".
+    ext_named_variadic_macro: see Section \"6.21 Macros with a Variable Number of Arguments\" of "GCC_MANUAL".
+    ext_return_has_void_expr: see the documentation for -Wreturn-type in Section \"3.8 Options to Request or Suppress Warnings\" of "GCC_MANUAL".
+    ext_gnu_statement_expr_macro: see Section \"6.1 Statements and Declarations in Expressions\" of "GCC_MANUAL".
+    ext_sizeof_alignof_void_type: see Section \"6.24 Arithmetic on void- and Function-Pointers\" of "GCC_MANUAL".
+    ext_forward_ref_enum_def: see Section \"6.49 Incomplete enum Types\" of "GCC_MANUAL".
+    ext_flexible_array_in_struct: see Section \"6.18 Arrays of Length Zero\" of "GCC_MANUAL".
+    ext_flexible_array_in_array: see Section \"6.18 Arrays of Length Zero\" of "GCC_MANUAL".
+    ext_enum_value_not_int: non-documented GCC extension.
+    ext_gnu_array_range: see Section \"6.29 Designated Initializers\" of "GCC_MANUAL".
+"
+-config=STD.diag,behavior+={c99,GCC_ARM64,"^(ext_paste_comma|ext_missing_varargs_arg|ext_named_variadic_macro|ext_return_has_void_expr|ext_gnu_statement_expr_macro|ext_sizeof_alignof_void_type|ext_forward_ref_enum_def|ext_gnu_array_range)$"}
+-config=STD.diag,behavior+={c99,GCC_X86_64,"^(ext_paste_comma|ext_missing_varargs_arg|ext_named_variadic_macro|ext_return_has_void_expr|ext_gnu_statement_expr_macro|ext_sizeof_alignof_void_type|ext_flexible_array_in_struct|ext_flexible_array_in_array|ext_enum_value_not_int|ext_gnu_array_range)$"}
+-doc_end
+
+-doc_begin="The maximum size of an object is defined in the MAX_SIZE macro, and for a 32 bit architecture is 8MB.
+    The maximum size for an array is defined in the PTRDIFF_MAX and in a 32 bit architecture is 2^30-1.
+    See occurrences of these macros in "GCC_MANUAL"."
+-config=STD.byteobjt,behavior+={c99, GCC_ARM64, 8388608}
+-config=STD.byteobjt,behavior+={c99, GCC_X86_64, 8388608}
+-doc_end
+
+-doc_begin="See Section \"11.2 Implementation limits\" of "CPP_MANUAL"."
+-config=STD.charline,behavior+={c99, GCC_ARM64, 5000}
+-config=STD.charline,behavior+={c99, GCC_X86_64, 12000}
+-doc_end
+
+-doc_begin="See Section \"11.2 Implementation limits\" of "CPP_MANUAL"."
+-config=STD.inclnest,behavior+={c99, GCC_ARM64, 24}
+-config=STD.inclnest,behavior+={c99, GCC_X86_64, 32}
+-doc_end
+
+-doc_begin="FIXME: why is C90 used?"
+-config=STD.ppifnest,behavior+={c90, GCC_X86_64, 32}
+-doc_end
+
+-doc_begin="See Section \"4.12 Statements\" of "GCC_MANUAL"."
+-config=STD.caselimt,behavior+={c99, GCC_X86_64, 1500}
+-doc_end
+
+-doc_begin="See Section \"6.9 128-bit Integers\" of "GCC_MANUAL"."
+-config=STD.stdtypes,behavior+={c99, GCC_X86_64, "__uint128_t"}
+-doc_end
+
+-doc_begin="FIXME: Non-documented GCC extension?"
+-config=STD.charescp,behavior={c99, GCC_X86_64, "^m$"}
+-doc_end
+
+-doc_begin="See Section \"4.9 Structures, Unions, Enumerations, and Bit-Fields\" of "GCC_MANUAL"."
+-config=STD.bitfldtp, +behavior={c99, GCC_ARM64, "unsigned char;unsigned short;unsigned long;unsigned long long"}
+-config=STD.bitfldtp, +behavior={c99, GCC_X86_64, "unsigned char;unsigned short;unsigned long;enum"}
+-doc_end
+
+-doc_begin="
+    #pragma pack: see Section \"6.62.11 Structure-Layout Pragmas\" of "GCC_MANUAL".
+    #pragma GCC visibility: see Section \"6.62.14 Visibility Pragmas\" of "GCC_MANUAL".
+"
+-config=STD.nonstdc,behavior={c99, GCC_ARM64, "^(pack\\(|GCC visibility (push|pop)).*$"}
+-config=STD.nonstdc,behavior={c99, GCC_X86_64, "^(pack\\(|GCC visibility (push|pop)).*$"}
+-doc_end
+
+-doc_begin="See Section \"1.1 Character sets\" of "CPP_MANUAL".  We assume the locale is not restricting any UTF-8 characters being part of the source character set."
+-config=STD.charset,behavior={c99, GCC_ARM64, "utf8"}
+-doc_end
+
+-doc_begin="See Section \"4.3 Identifiers\" of "GCC_MANUAL"."
+-config=STD.extidsig, behavior+={c99, GCC_ARM64, "63"}
+-config=STD.extidsig, behavior+={c99, GCC_X86_64, "63"}
+-doc_end
+
+#
+# Documentation for relied-upon implementation-defined behaviors (Dir 1.1)
+#
+
+-doc_begin="See Section \"4.4 Characters\" of "GCC_MANUAL" and Section \"8.1 Data types\" of "ARM64_ABI_MANUAL"."
+-config=STD.bytebits,behavior={c99, GCC_ARM64, "8"}
+-config=STD.charsobj,behavior={c99, GCC_ARM64, "utf8"}
+-config=STD.charsval,behavior={c99, GCC_ARM64, "utf8"}
+-doc_end
+
+-doc_begin="See Section \"4.4 Characters\" of "GCC_MANUAL" and Section \"3.1.2 Data Representation\" of "X86_64_ABI_MANUAL"."
+-config=STD.bytebits,behavior={c99, GCC_X86_64, "8"}
+-config=STD.charsobj,behavior={c99, GCC_X86_64, "utf8"}
+-config=STD.charsval,behavior={c99, GCC_X86_64, "utf8"}
+-doc_end
+
+-doc_begin="See Section \"4.4 Characters\" of "GCC_MANUAL" and the documentation for -finput-charset=charset in the same manual."
+-config=STD.charsmap,behavior={c99, GCC_ARM64, "specified"}
+-config=STD.charsmap,behavior={c99, GCC_X86_64, "specified"}
+-doc_end
+
+-doc_begin="See Section \"4.4 Characters\" of "GCC_MANUAL" and the documentation for -fexec-charset=charset and -finput-charset=charset in the same manual."
+-config=STD.charsmem,behavior={c99, GCC_ARM64, "utf8"}
+-config=STD.charsmem,behavior={c99, GCC_X86_64, "utf8"}
+-doc_end
+
+-doc_begin="See Section \"4.1 Translation\" of "GCC_MANUAL"."
+-config=STD.diagidnt,behavior={c99, GCC_ARM64, "specified"}
+-config=STD.diagidnt,behavior={c99, GCC_X86_64, "specified"}
+-doc_end
+
+-doc_begin="See Section \"4.4 Characters\" of "GCC_MANUAL" and the documentation for -fexec-charset=charset in the same manual."
+-config=STD.execvals,behavior={c99, GCC_ARM64, "specified"}
+-config=STD.execvals,behavior={c99, GCC_X86_64, "specified"}
+-doc_end
+
+-doc_begin="Given that Xen is compiled in hosted mode, ECLAIR cannot exclude the independency from program termination implementation-defined behavior.  See \"Section 25.7 Program Termination\" of "ARM64_LIBC_MANUAL"."
+-config=STD.exitstat,behavior={c99, GCC_ARM64, "specified"}
+-doc_end
+
+-doc_begin="Given that Xen is compiled in hosted mode, ECLAIR cannot exclude the independency from program termination implementation-defined behavior.  See \"Section 25.7 Program Termination\" of "X86_64_LIBC_MANUAL"."
+-config=STD.exitstat,behavior={c99, GCC_X86_64, "specified"}
+-doc_end
+
+-doc_begin="See Chapter \"2 Header Files\" of "CPP_MANUAL"."
+-config=STD.inclangl,behavior={c99, GCC_ARM64, "specified"}
+-config=STD.inclangl,behavior={c99, GCC_X86_64, "specified"}
+-config=STD.inclfile,behavior={c99, GCC_ARM64, "specified"}
+-config=STD.inclfile,behavior={c99, GCC_X86_64, "specified"}
+-config=STD.inclhead,behavior={c99, GCC_ARM64, "specified"}
+-config=STD.inclhead,behavior={c99, GCC_X86_64, "specified"}
+-doc_end
+
+-doc_begin="See Section \"4.5 Integers\" of "GCC_MANUAL"."
+-config=STD.signdint,behavior={c99, GCC_ARM64, "specified"}
+-config=STD.signdint,behavior={c99, GCC_X86_64, "specified"}
+-doc_end
+
+-doc_begin="See Section \"4.15 Architecture\" of "GCC_MANUAL" and Chapter \"5   Data types and alignment\" of "ARM64_ABI_MANUAL"."
+-config=STD.objbytes,behavior={c99, GCC_ARM64, "specified"}
+-doc_end
+
+-doc_begin="See Section \"4.15 Architecture\" of "GCC_MANUAL" and Section \"3.1.2 Data Representation\" of "X86_64_ABI_MANUAL"."
+-config=STD.objbytes,behavior={c99, GCC_X86_64, "specified"}
+-doc_end
+
+-doc_begin="See Section \"3.4 Stringizing\" of "CPP_MANUAL"."
+-config=STD.stringfy,behavior={c99, GCC_ARM64, "specified"}
+-config=STD.stringfy,behavior={c99, GCC_X86_64, "specified"}
+-doc_end
+
+-doc_begin="See Section \"4.9 Structures, Unions, Enumerations, and Bit-Fields\"
+ of "GCC_MANUAL" and Section \"8.1.8 Bit-fields\" of "ARM64_ABI_MANUAL"."
+-config=STD.bitfldby,+behavior={c99, GCC_ARM64, "specified"}
+-config=STD.bitfldor,+behavior={c99, GCC_ARM64, "specified"}
+-doc_end
+
+-doc_begin="See Section \"4.9 Structures, Unions, Enumerations, and Bit-Fields\"
+ of "GCC_MANUAL" and Section \"3.1.2 Data Representation\" of "X86_64_ABI_MANUAL"."
+-config=STD.bitfldby,+behavior={c99, GCC_X86_64, "specified"}
+-config=STD.bitfldor,+behavior={c99, GCC_X86_64, "specified"}
+-doc_end
+
+-doc_begin="See Section \"4.10 Qualifiers\" of "GCC_MANUAL"."
+-config=STD.volatltp,+behavior={c99, GCC_ARM64, "specified"}
+-config=STD.volatltp,+behavior={c99, GCC_X86_64, "specified"}
+-doc_end
+
+-doc_begin="See Section \"4.15 Architecture\" of "GCC_MANUAL" and Chapter \"5   Data types and alignment\" of "ARM64_ABI_MANUAL"."
+-config=STD.stdmacro,behavior={c99, GCC_ARM64, "specified"}
+-doc_end
+
+-doc_begin="See Section \"4.15 Architecture\" of "GCC_MANUAL" and Section \"3.1.2 Data Representation\" of "X86_64_ABI_MANUAL"."
+-config=STD.stdmacro,behavior={c99, GCC_X86_64, "specified"}
+-doc_end
+
+-doc_begin="See Section \"4.4 Characters\" of "GCC_MANUAL" and Section \"11.1 Implementation-defined behavior\" of "CPP_MANUAL"."
+-config=STD.widestng,behavior={c99, GCC_ARM64, "specified"}
+-config=STD.widestng,behavior={c99, GCC_X86_64, "specified"}
+-config=STD.multbtsl,behavior={c99, GCC_X86_64, "specified"}
+-doc_end
+
+-doc_begin="See Section \"4.13 Preprocessing Directives\" of "GCC_MANUAL" and Section \"7 Pragmas\" of "CPP_MANUAL"."
+-config=STD.pragmdir,behavior={c99, GCC_ARM64, "^(pack\\(|GCC visibility (push|pop)).*$"}
+-config=STD.pragmdir,behavior={c99, GCC_X86_64, "^(pack\\(|GCC visibility (push|pop)).*$"}
+-doc_end
+
+-doc_begin="See Section \"6.9 128-bit Integers\" of "GCC_MANUAL"."
+-config=STD.extinttp,behavior={c99, GCC_X86_64, "__uint128_t"}
+-doc_end
+
+-doc_begin="See Section \"4.13 Preprocessing Directives\" of "GCC_MANUAL" and Section \"11.1 Implementation-defined behavior\" of "CPP_MANUAL"."
+-config=STD.inclexpd,behavior={c99, GCC_X86_64, "specified"}
+-doc_end