From 89bb946727e0eba9bd5a0eab6f912e28cf39b8a6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 25 Oct 2019 13:21:09 +0200
Subject: [PATCH] [markdown] refactor example into tests
---
src/libraries/utils/markdown.ml | 13 +--
.../tests/eva/oracle/cwe126.0.md | 3 +-
.../tests/eva/result/cwe126.0.md | 95 -------------------
3 files changed, 8 insertions(+), 103 deletions(-)
delete mode 100644 src/plugins/markdown-report/tests/eva/result/cwe126.0.md
diff --git a/src/libraries/utils/markdown.ml b/src/libraries/utils/markdown.ml
index f442f675935..d86a51b1f06 100644
--- a/src/libraries/utils/markdown.ml
+++ b/src/libraries/utils/markdown.ml
@@ -328,12 +328,12 @@ let pp_table_extended ?page fmt { caption; header; content } =
let pp_table_inlined ?page fmt { caption; header; content } =
begin
pp_table_caption ?page fmt caption;
- Format.fprintf fmt "@[<v>";
let pp = pp_text ?page in
+ Format.fprintf fmt "@[<v>@[<h>";
List.iter
- (function (h,_) -> Format.fprintf fmt "| @[<h>%a@] " pp h)
+ (function (h,_) -> Format.fprintf fmt "| %a " pp h)
header;
- Format.fprintf fmt "|@\n";
+ Format.fprintf fmt "|@]@\n@[<h>";
List.iter
(fun (h,align) ->
let dash h k = String.make (max 3 (test_size ?page h + k)) '-' in
@@ -342,11 +342,12 @@ let pp_table_inlined ?page fmt { caption; header; content } =
| Right -> Format.fprintf fmt "|%s:" (dash h 1)
| Center -> Format.fprintf fmt "|:%s:" (dash h 0)
) header;
- Format.fprintf fmt "|@\n" ;
+ Format.fprintf fmt "|@]@\n" ;
List.iter (fun row ->
+ Format.fprintf fmt "@[<h>" ;
List.iter
- (fun col -> Format.fprintf fmt "| @[<h>%a@] " pp col) row ;
- Format.fprintf fmt "|@\n" ;
+ (fun col -> Format.fprintf fmt "| %a " pp col) row ;
+ Format.fprintf fmt "|@]@\n" ;
) content ;
Format.fprintf fmt "@]" ;
end
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 382c657cb9b..3d766a9a0d7 100644
--- a/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md
+++ b/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md
@@ -81,8 +81,7 @@ Table: Alarm emitted by the analysis
| No | Kind | Emitter | Function | Location |
|:---:|:----:|:-------:|:---------|:---------|
-| [0](#alarm-0) | mem_access | Eva | CWE126_Buffer_Overread__malloc_char_loop_64b_badSink |
-tests/eva/cwe126.c:24 |
+| [0](#alarm-0) | mem_access | Eva | CWE126_Buffer_Overread__malloc_char_loop_64b_badSink | tests/eva/cwe126.c:24 |
## Alarm 0 at tests/eva/cwe126.c:24 {#Alarm-0}
diff --git a/src/plugins/markdown-report/tests/eva/result/cwe126.0.md b/src/plugins/markdown-report/tests/eva/result/cwe126.0.md
deleted file mode 100644
index 382c657cb9b..00000000000
--- a/src/plugins/markdown-report/tests/eva/result/cwe126.0.md
+++ /dev/null
@@ -1,95 +0,0 @@
----
-title: Frama-C Analysis Report
-author:
-date: 2019-10-25
-...
-
-\let\underscore\_
-\renewcommand{\_}{\discretionary{\underscore}{}{\underscore}}
-
-# Context of the analysis {#context}
-
-## Input files {#c-input}
-
-The C source files (not including the headers `.h` files)
-that have been considered during the analysis are the following:
-
-* `tests/eva/*.c`
-
-
-
-## Configuration {#options}
-
-The options that have been used for this analysis are the following.
-
-
-### EVA Domains {#domains}
-
-Only the base domain (`Cvalue`) has been used for the analysis
-
-
-### Stubbed Functions {#stubs}
-
-No stubs have been used for this analysis
-
-
-# Coverage {#coverage}
-
-There are 6 function definitions that are not stubbed. They represent 50 statements, of which 50 are potentially reachable through EVA, resulting in a **statement coverage of 100.0%** with respect to the entire application.
-
-
-There were potentially 6 functions syntactically reachable from main.
-These functions contain 50 statements, of which 50 are potentially reachable according to EVA, resulting in a **statement coverage of 100.0%** with respect to the perimeter set by this entry point.
-
-
-# Warnings {#warnings}
-
-The table below lists the warning that have been emitted by the analyzer.
-They might put additional assumptions on the relevance
-of the analysis results and must be reviewed carefully
-
-Note that this does not take into account emitted alarms:
-they are reported in [the next section](#alarms)
-
-
-
-Table: Warning reported by Frama-C
-
-| Location | Description |
-|:---------|:------------|
-| tests/eva/cwe126.c:24 | `out of bounds read. assert \valid_read(data + i);` (emitted by `eva`) |
-
-
-## Warning 0 (tests/eva/cwe126.c:24) {#warn-0}
-
-```log
-Message: out of bounds read. assert \valid_read(data + i);
-```
-
-
-# Results of the analysis {#alarms}
-
-The table below lists the alarm that have been emitted during the analysis.
-Any execution starting from `main`
-in a context matching the one used for the analysis
-will be immune from any other undefined behavior.
-More information on each individual alarm is
-given in the remainder of this section
-
-
-Table: Alarm emitted by the analysis
-
-| No | Kind | Emitter | Function | Location |
-|:---:|:----:|:-------:|:---------|:---------|
-| [0](#alarm-0) | mem_access | Eva | CWE126_Buffer_Overread__malloc_char_loop_64b_badSink |
-tests/eva/cwe126.c:24 |
-
-
-## Alarm 0 at tests/eva/cwe126.c:24 {#Alarm-0}
-
-The following ACSL assertion must hold to avoid an undefined behavior (mem_access)
-
-```acsl
-assert mem_access: \valid_read(data + i);
-```
-
--
GitLab