Skip to content
Snippets Groups Projects
Commit adaf7cc2 authored by Loïc Correnson's avatar Loïc Correnson Committed by Virgile Prevosto
Browse files

[markdown] refactor example into tests

parent d410b6f5
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 410 additions and 149 deletions
src/plugins/markdown-report/Makefile
+ 1
− 1
View file @ adaf7cc2
......@@ -9,10 +9,10 @@ PLUGIN_GENERATED:=$(PLUGIN_DIR)/mdr_version.ml $(PLUGIN_DIR)/Report_markdown.mli
PLUGIN_CMO:=\
sarif mdr_version mdr_params parse_remarks \
eva_coverage md_gen sarif_gen mdr_register
PLUGIN_NO_TEST:=true
PLUGIN_REQUIRES:=ppx_deriving ppx_deriving_yojson yojson
PLUGIN_VERSION:=$(Report_markdown_VERSION)
PLUGIN_DISTRIB_EXTERNAL:=share/acsl.xml
PLUGIN_TESTS_DIRS:= eva
include $(FRAMAC_SHARE)/Makefile.dynamic
......
src/plugins/markdown-report/tests/eva/cwe126.md 0 → 100644
+ 139
− 0
View file @ adaf7cc2
---
title: Draft report
author:
date: 2019-10-25
...
\let\underscore\_
\renewcommand{\_}{\discretionary{\underscore}{}{\underscore}}
<!-- This file contains additional remarks that will be added to
automatically generated content by Frama-C's Markdown-report plugin. For
any section of the document, you can write pandoc markdown content
between the BEGIN and END comments. In addition, the plug-in will
consider any \<!-- INCLUDE file.md --\> comment (without backslashes) as
a directive to include the content of file.md in the corresponding
section. Please don't alter the structure of the document as it is used
by the plugin to associate content to the relevant section.
-->
# Introduction {#intro}
<!-- You can add here some overall introduction to the analysis -->
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
# Context of the analysis {#context}
## Input files {#c-input}
<!-- You can add here some remarks about the set of files that is considered
by Frama-C
-->
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
The C source files (not including the headers `.h` files)
that have been considered during the analysis are the following:
* `./*.c`
## Configuration {#options}
<!-- You can add here some remarks about the options used for the analysis
-->
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
### EVA Domains {#domains}
<!-- You can give more information about the choice of EVA domains -->
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
### Stubbed Functions {#stubs}
<!-- You can add here general comments about the stubs that have been used
-->
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
<!-- No stubs have been used -->
# 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.
<!-- You can comment on the coverage obtained by EVA -->
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
# Errors in the analyzer {#errors}
<!-- you can comment on each individual error -->
## Error 0 (Global) {#err-0}
```log
Message: Unable to open remarks file cwe126.remarks-sample.md (cwe126.remarks-sample.md: No such file or directory). No additional remarks will be included in the report.
```
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
# Warnings {#warnings}
<!-- you can comment on each individual error -->
## Warning 0 (cwe126.c:24) {#warn-0}
```log
Message: out of bounds read. assert \valid_read(data + i);
```
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
# Results of the analysis {#alarms}
## Alarm 0 at cwe126.c:24 {#Alarm-0}
```acsl
assert mem_access: \valid_read(data + i);
```
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
# Conclusion {#conclusion}
<!-- You can put here some concluding remarks -->
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
\ No newline at end of file
src/plugins/markdown-report/examples/cwe126.remarks-sample.md → src/plugins/markdown-report/tests/eva/cwe126.remarks.md
+ 13
− 148
View file @ adaf7cc2
---
title: Draft report
author:
date: 2018-12-13
date: 2019-10-25
...
\let\underscore\_
......@@ -22,9 +22,11 @@ date: 2018-12-13
<!-- You can add here some overall introduction to the analysis -->
<!-- BEGIN_REMARK -->
This is a test from the Juliet test suite showing an example of buffer
overflow (CWE126). The `good` functions should not trigger any alarm, while
the `bad` ones have indeed an error.
<!-- END_REMARK -->
# Context of the analysis {#context}
......@@ -42,7 +44,7 @@ the `bad` ones have indeed an error.
The C source files (not including the headers `.h` files)
that have been considered during the analysis are the following:
* `cwe126.c`
* `./*.c`
......@@ -72,152 +74,15 @@ that have been considered during the analysis are the following:
<!-- END_REMARK -->
<!-- You can add here general comments about the stubs that have been used
-->
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `char_equal_ignore_case` {#char_equal_ignore_case}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `memrchr` {#memrchr}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `strcasecmp` {#strcasecmp}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `strndup` {#strndup}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `strdup` {#strdup}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `strncat` {#strncat}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `strcat` {#strcat}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `strncpy` {#strncpy}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `strcpy` {#strcpy}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `strerror` {#strerror}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `strstr` {#strstr}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `strrchr` {#strrchr}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `strchr` {#strchr}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `strncmp` {#strncmp}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `strcmp` {#strcmp}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `strnlen` {#strnlen}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `strlen` {#strlen}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `memset` {#memset}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `memmove` {#memmove}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `memcpy` {#memcpy}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `memchr` {#memchr}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
#### `memcmp` {#memcmp}
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
<!-- No stubs have been used -->
# Coverage {#coverage}
There are 6 function definitions that are not stubbed. They represent 50 statements, of which 43 are potentially reachable through EVA, resulting in a **statement coverage of 86.0%** with respect to the entire application.
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 43 are potentially reachable according to EVA, resulting in a **statement coverage of 86.0%** with respect to the perimeter set by this entry point.
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.
<!-- You can comment on the coverage obtained by EVA -->
......@@ -232,10 +97,9 @@ These functions contain 50 statements, of which 43 are potentially reachable acc
## Warning 0 (cwe126.c:24) {#warn-0}
message text is
out of bounds read. assert \valid_read(data + i);
```log
Message: out of bounds read. assert \valid_read(data + i);
```
<!-- BEGIN_REMARK -->
......@@ -252,8 +116,10 @@ assert mem_access: \valid_read(data + i);
<!-- BEGIN_REMARK -->
This alarm is real: Eva correctly identified the issue and did not report
any spurious alarm anywhere else.
<!-- END_REMARK -->
# Conclusion {#conclusion}
......@@ -262,5 +128,4 @@ any spurious alarm anywhere else.
<!-- BEGIN_REMARK -->
<!-- END_REMARK -->
<!-- END_REMARK -->
\ No newline at end of file
src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md 0 → 100644
+ 95
− 0
View file @ adaf7cc2
---
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);
```
src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle 0 → 100644
+ 57
− 0
View file @ adaf7cc2
[kernel] Parsing tests/eva/cwe126.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva] tests/eva/cwe126.c:72: allocating variable __malloc_goodG2B_l72
[eva] using specification for function exit
[eva] FRAMAC_SHARE/libc/string.h:118:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
[eva] tests/eva/cwe126.c:58: starting to merge loop iterations
[eva] tests/eva/cwe126.c:36:
allocating variable __malloc_CWE126_Buffer_Overread__malloc_char_loop_64_bad_l36
[eva] tests/eva/cwe126.c:22: starting to merge loop iterations
[eva:alarm] tests/eva/cwe126.c:24: Warning:
out of bounds read. assert \valid_read(data + i);
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states]
Values at end of function CWE126_Buffer_Overread__malloc_char_loop_64b_badSink:
dataPtr ∈ {{ &data }}
data ∈ ESCAPINGADDR
data ∈ ESCAPINGADDR
[eva:final-states]
Values at end of function CWE126_Buffer_Overread__malloc_char_loop_64_bad:
__fc_heap_status ∈ [--..--]
data ∈ ESCAPINGADDR
[eva:final-states]
Values at end of function CWE126_Buffer_Overread__malloc_char_loop_64b_goodG2BSink:
dataPtr ∈ {{ &data }}
data ∈ ESCAPINGADDR
data ∈ ESCAPINGADDR
[eva:final-states] Values at end of function goodG2B:
__fc_heap_status ∈ [--..--]
data ∈ ESCAPINGADDR
[eva:final-states]
Values at end of function CWE126_Buffer_Overread__malloc_char_loop_64_good:
__fc_heap_status ∈ [--..--]
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
__retres ∈ {0}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
6 functions analyzed (out of 6): 100% coverage.
In these functions, 54 statements reached (out of 54): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
1 alarm generated by the analysis:
1 invalid memory access
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
Assertions 0 valid 0 unknown 0 invalid 0 total
Preconditions 8 valid 0 unknown 0 invalid 8 total
100% of the logical properties reached have been proven.
----------------------------------------------------------------------------
[mdr] Report tests/eva/result/cwe126.0.md generated
src/plugins/markdown-report/tests/eva/result/cwe126.0.md 0 → 100644
+ 95
− 0
View file @ adaf7cc2
---
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);
```
src/plugins/markdown-report/tests/eva/test_config 0 → 100644
+ 3
− 0
View file @ adaf7cc2
CMD: @frama-c@ -eva @PTEST_FILE@ -mdr-gen md -mdr-out @PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.md
LOG: @PTEST_NAME@.@PTEST_NUMBER@.md
OPT:
src/plugins/markdown-report/tests/ptests_config 0 → 100644
+ 7
− 0
View file @ adaf7cc2
DEFAULT_SUITES= eva
TOPLEVEL_PATH=/Users/correnson/Frama-C/trunk/bin/toplevel.opt
FRAMAC_SHARE=/Users/correnson/Frama-C/trunk/share
FRAMAC_LIB=/Users/correnson/Frama-C/trunk/lib/fc
FRAMAC_PLUGIN=/Users/correnson/Frama-C/trunk/lib/plugins
FRAMAC_PLUGIN_GUI=/Users/correnson/Frama-C/trunk/lib/plugins/gui
OCAMLRUNPARAM=
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment