From e02997ec7d7bd1792be159f78304ed4d4cd64c1b Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 6 Dec 2017 11:33:28 +0100
Subject: [PATCH] Don't forget to add remarks over stub functions in the final
document
---
src/plugins/markdown-report/md_gen.ml | 15 +++++++++------
1 file changed, 9 insertions(+), 6 deletions(-)
diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml
index ed6f85bd856..12322e06cb3 100644
--- a/src/plugins/markdown-report/md_gen.ml
+++ b/src/plugins/markdown-report/md_gen.ml
@@ -102,12 +102,15 @@ let section_stubs env =
let kf = Globals.Functions.find_by_name s in
let content =
if env.is_draft then insert_marks
- else
- [ Block
- [ Text
- [Inline_code s; Plain "has the following specification"];
- codelines
- "acsl" Printer.pp_funspec (Annotations.funspec kf)]]
+ else begin
+ let comment = insert_remark env s in
+ Block
+ [ Text
+ [Inline_code s; Plain "has the following specification"];
+ codelines
+ "acsl" Printer.pp_funspec (Annotations.funspec kf)]
+ :: comment
+ end
in
H4 ([Inline_code s], Some s) :: content)
l
--
GitLab