From 102d9181ecd9289edd5905b820334261cce1939b Mon Sep 17 00:00:00 2001 From: Virgile Prevosto Date: Thu, 7 Apr 2022 18:15:21 +0200 Subject: [PATCH 1/6] Introducing LTest --- _fc-plugins/ltest.md | 51 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 _fc-plugins/ltest.md diff --git a/_fc-plugins/ltest.md b/_fc-plugins/ltest.md new file mode 100644 index 00000000..5dac5dcc --- /dev/null +++ b/_fc-plugins/ltest.md @@ -0,0 +1,51 @@ +--- +layout: plugin +title: LTest +description: Set of utilities for test coverage +key: reporting +distrib_mode: free +--- + +## Overview + +LTest is composed of two Frama-C plugins, `LAnnotate` and `LUncov`, +and one external executable, `LReplay`, that aim at providing +accurate test coverage metrics for a wide range of coverage criteria. + +More specifically, they are based on _labels_ and _hyperlabels_, +which formalizes the notion of _test objectives_ that must be +covered for a given criterion. In this context, + +- `LAnnotate` generates the set of (hyper)labels corresponding to + the selected criteria for a given C program; +- `LUncov` attempts to detect the (hyper)labels that are unreachable, + and the ones that are redundant; +- `LReplay` executes a test suite over some code instrumented with + (hyper)labels and computes a coverage ratio. + +## Further Reading + +- Sébastien Bardin, Nikolai Kosmatov, Michaël Marcozzi, and Mickaël Delahaye. + _Specify and Measure, Cover and Reveal: A Unified Framework for Automated Test Generation._ + In _Science of Computer Programming_, 2021, vol. 207, ISSN 0167-6423. +  [DOI: 10.1016/j.scico.2021.102641](https://doi.org/10.1016/j.scico.2021.102641) +- Michaël Marcozzi, Mickaël Delahaye, Sébastien Bardin, Nikolai Kosmatov and Virgile Prevosto. + _Generic and Effective Specification of Structural Test Objectives._ + In _Proc. of the 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017)_, Tokyo, Japan, March 2017, pages 436-441. IEEE. ISBN 978-1-5090-6031-3. + [DOI: 10.1109/ICST.2017.57](https://doi.org/10.1109/ICST.2017.57) + +## Installation + +All three packages are available in `opam` and can be installed trough + +``` +opam install frama-c-lannotate frama-c-luncov lreplay +``` + +Manual installation instructions are available in the README of each of the repositories: + +- [https://git.frama-c.com/pub/ltest/lannotate](https://git.frama-c.com/pub/ltest/lannotate) +- [https://git.frama-c.com/pub/ltest/luncov](https://git.frama-c.com/pub/ltest/luncov) +- [https://git.frama-c.com/pub/ltest/lreplay](https://git.frama-c.com/pub/ltest/lreplay) + +They require OCaml>= 4.08.1, and, for the plugins, Frama-C 24.0 Chromium -- GitLab From df80e47c48ab65c342077bcceac8caeef19c3f34 Mon Sep 17 00:00:00 2001 From: Virgile Prevosto Date: Thu, 7 Apr 2022 16:37:29 +0000 Subject: [PATCH 2/6] Update ltest.md following review --- _fc-plugins/ltest.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/_fc-plugins/ltest.md b/_fc-plugins/ltest.md index 5dac5dcc..18e761af 100644 --- a/_fc-plugins/ltest.md +++ b/_fc-plugins/ltest.md @@ -13,7 +13,7 @@ and one external executable, `LReplay`, that aim at providing accurate test coverage metrics for a wide range of coverage criteria. More specifically, they are based on _labels_ and _hyperlabels_, -which formalizes the notion of _test objectives_ that must be +which formalize the notion of _test objectives_ that must be covered for a given criterion. In this context, - `LAnnotate` generates the set of (hyper)labels corresponding to -- GitLab From f3c1e7ac6b5219772467b08ec4d71e72c2fe003d Mon Sep 17 00:00:00 2001 From: Virgile Prevosto Date: Thu, 7 Apr 2022 16:41:02 +0000 Subject: [PATCH 3/6] Update ltest.md following review --- _fc-plugins/ltest.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/_fc-plugins/ltest.md b/_fc-plugins/ltest.md index 18e761af..1bc0ed68 100644 --- a/_fc-plugins/ltest.md +++ b/_fc-plugins/ltest.md @@ -18,7 +18,7 @@ covered for a given criterion. In this context, - `LAnnotate` generates the set of (hyper)labels corresponding to the selected criteria for a given C program; -- `LUncov` attempts to detect the (hyper)labels that are unreachable, +- `LUncov` attempts to detect the (hyper)labels that are uncoverable, and the ones that are redundant; - `LReplay` executes a test suite over some code instrumented with (hyper)labels and computes a coverage ratio. -- GitLab From 0de002ffd496d722973bb0b2f5164c182b949f82 Mon Sep 17 00:00:00 2001 From: Virgile Prevosto Date: Fri, 8 Apr 2022 08:36:48 +0200 Subject: [PATCH 4/6] [ltest] Add reference to pathcrawler --- _fc-plugins/ltest.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/_fc-plugins/ltest.md b/_fc-plugins/ltest.md index 1bc0ed68..1431014b 100644 --- a/_fc-plugins/ltest.md +++ b/_fc-plugins/ltest.md @@ -23,6 +23,11 @@ covered for a given criterion. In this context, - `LReplay` executes a test suite over some code instrumented with (hyper)labels and computes a coverage ratio. +On the other hand, these component, and notably `LReplay` assume that you +already have a test suite whose coverage you want to evaluate. Still in the +context of Frama-C, you can for instance use +[PathCrawler]({% link _fc-plugins/pathcrawler.md %}) to generate such a suite. + ## Further Reading - Sébastien Bardin, Nikolai Kosmatov, Michaël Marcozzi, and Mickaël Delahaye. -- GitLab From 73b62c1d949b762a837c3bde325b6f6a41119d6b Mon Sep 17 00:00:00 2001 From: Virgile Prevosto Date: Fri, 8 Apr 2022 09:32:33 +0200 Subject: [PATCH 5/6] [ltest] fix typos from review --- _fc-plugins/ltest.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/_fc-plugins/ltest.md b/_fc-plugins/ltest.md index 1431014b..51008a15 100644 --- a/_fc-plugins/ltest.md +++ b/_fc-plugins/ltest.md @@ -23,7 +23,7 @@ covered for a given criterion. In this context, - `LReplay` executes a test suite over some code instrumented with (hyper)labels and computes a coverage ratio. -On the other hand, these component, and notably `LReplay` assume that you +On the other hand, these components, and notably `LReplay` assume that you already have a test suite whose coverage you want to evaluate. Still in the context of Frama-C, you can for instance use [PathCrawler]({% link _fc-plugins/pathcrawler.md %}) to generate such a suite. @@ -41,7 +41,7 @@ context of Frama-C, you can for instance use ## Installation -All three packages are available in `opam` and can be installed trough +All three packages are available in `opam` and can be installed through ``` opam install frama-c-lannotate frama-c-luncov lreplay @@ -53,4 +53,4 @@ Manual installation instructions are available in the README of each of the repo - [https://git.frama-c.com/pub/ltest/luncov](https://git.frama-c.com/pub/ltest/luncov) - [https://git.frama-c.com/pub/ltest/lreplay](https://git.frama-c.com/pub/ltest/lreplay) -They require OCaml>= 4.08.1, and, for the plugins, Frama-C 24.0 Chromium +They require OCaml>= 4.08.1, and, for the plugins, Frama-C 24.0 (Chromium). -- GitLab From f11007375cdc93b12c65dd2c34ee627dc0377910 Mon Sep 17 00:00:00 2001 From: Virgile Prevosto Date: Fri, 8 Apr 2022 10:55:16 +0200 Subject: [PATCH 6/6] [ltest] add some links --- _fc-plugins/ltest.md | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/_fc-plugins/ltest.md b/_fc-plugins/ltest.md index 51008a15..1ecaa317 100644 --- a/_fc-plugins/ltest.md +++ b/_fc-plugins/ltest.md @@ -28,6 +28,12 @@ already have a test suite whose coverage you want to evaluate. Still in the context of Frama-C, you can for instance use [PathCrawler]({% link _fc-plugins/pathcrawler.md %}) to generate such a suite. +These three tools are available on Frama-C's gitlab server under LGPL-2.1-only: +- [LAnnotate](https://git.frama-c.com/pub/ltest/lannotate) +- [LUncov](https://git.frama-c.com/pub/ltest/luncov) +- [LReplay](https://git.frama-c.com/pub/ltest/lreplay) + + ## Further Reading - Sébastien Bardin, Nikolai Kosmatov, Michaël Marcozzi, and Mickaël Delahaye. @@ -49,8 +55,8 @@ opam install frama-c-lannotate frama-c-luncov lreplay Manual installation instructions are available in the README of each of the repositories: -- [https://git.frama-c.com/pub/ltest/lannotate](https://git.frama-c.com/pub/ltest/lannotate) -- [https://git.frama-c.com/pub/ltest/luncov](https://git.frama-c.com/pub/ltest/luncov) -- [https://git.frama-c.com/pub/ltest/lreplay](https://git.frama-c.com/pub/ltest/lreplay) +- [LAnnotate](https://git.frama-c.com/pub/ltest/lannotate/-/blob/master/README.markdown) +- [LUncov](https://git.frama-c.com/pub/ltest/luncov/-/blob/master/README.markdown) +- [LReplay](https://git.frama-c.com/pub/ltest/lreplay/-/blob/master/README.markdown) They require OCaml>= 4.08.1, and, for the plugins, Frama-C 24.0 (Chromium). -- GitLab