From 125306aef44cd1ec9632ef243559f4fd014ec746 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 25 Oct 2019 15:04:34 +0200
Subject: [PATCH] [mdr] rephrasing alarms description
---
src/plugins/markdown-report/md_gen.ml | 16 +++++++++-------
.../markdown-report/tests/eva/oracle/cwe126.0.md | 3 ++-
2 files changed, 11 insertions(+), 8 deletions(-)
diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml
index a9081440d9c..a72088f49b7 100644
--- a/src/plugins/markdown-report/md_gen.ml
+++ b/src/plugins/markdown-report/md_gen.ml
@@ -452,11 +452,11 @@ let gen_section_warnings env =
let gen_section_alarms env =
let treat_alarm e kf s ~rank:_ alarm annot (i, sec, content) =
- let kind = Alarms.get_name alarm in
let label = "Alarm-" ^ string_of_int i in
let link = link ~text:(format "%d" i) ~name:label () in
- let func = code (Kernel_function.get_name kf) in
- let loc = string_of_loc (Cil_datatype.Stmt.loc s) in
+ let kind = code @@ Alarms.get_name alarm in
+ let func = code @@ Kernel_function.get_name kf in
+ let loc = string_of_loc @@ Cil_datatype.Stmt.loc s in
let loc_text = plain loc in
let emitter = code (Emitter.get_name e) in
let descr = codeblock "acsl" Printer.pp_code_annotation annot in
@@ -466,15 +466,17 @@ let gen_section_alarms env =
Block descr :: insert_marks env label
else
Block
- ( (text @@ format
- "The following ACSL assertion must hold to avoid \
- an undefined behavior (%s)" kind)
+ ( (text @@ glue [
+ plain "The following ACSL assertion must hold to avoid" ;
+ plain (Alarms.get_description alarm |> String.lowercase_ascii) ;
+ format "(undefined behavior)."
+ ])
@ descr )
:: insert_remark env label
in
(i+1,
sec @ H2 (sec_title, Some label) :: sec_content,
- [ link; code kind; emitter; func; loc_text ] :: content)
+ [ link; kind; emitter; func; loc_text ] :: content)
in
let _,sections, content = Alarms.fold treat_alarm (0,[],[]) in
let content = List.rev content in
diff --git a/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md b/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md
index 7407b142971..bfafd8867c7 100644
--- a/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md
+++ b/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md
@@ -89,7 +89,8 @@ Table: Alarm emitted by the analysis
## Alarm 0 at tests/eva/cwe126.c:28 {#Alarm-0}
-The following ACSL assertion must hold to avoid an undefined behavior (mem_access)
+The following ACSL assertion must hold to avoid invalid pointer dereferencing
+(undefined behavior).
```acsl
assert mem_access: \valid_read(data + i);
--
GitLab