Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
Frama-C Website
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Container Registry
Operate
Environments
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
Frama-C Website
Merge requests
!148
[blog] post about LTest opam release
Code
Review changes
Check out branch
Download
Patches
Plain diff
Merged
[blog] post about LTest opam release
blog-ltest-opam
into
master
Overview
5
Commits
1
Pipelines
4
Changes
1
1 unresolved thread
Show all comments
Merged
Andre Maroneze
requested to merge
blog-ltest-opam
into
master
2 years ago
Overview
5
Commits
1
Pipelines
4
Changes
1
1 unresolved thread
Show all comments
Expand
0
0
Merge request reports
Compare
master
version 3
fe1fa8b0
2 years ago
version 2
b7fe00be
2 years ago
version 1
fe1fa8b0
2 years ago
master (base)
and
version 1
latest version
b0f031ca
1 commit,
2 years ago
version 3
fe1fa8b0
1 commit,
2 years ago
version 2
b7fe00be
2 commits,
2 years ago
version 1
fe1fa8b0
1 commit,
2 years ago
1 file
+
51
−
0
Inline
Compare changes
Side-by-side
Inline
Show whitespace changes
Show one file at a time
_posts/2022-04-xx-ltest-plugins-released.md
0 → 100644
+
51
−
0
Options
---
layout
:
post
author
:
André Maroneze (review by Virgile Prevosto)
date
:
2022-04-xx 12:00 +0100
categories
:
test
title
:
"
Test
plug-ins
(re-)released:
LUncov,
LAnnotate,
LReplay
(all
part
of
LTest)"
---
The Ltest "meta-plugin" (composed of three parts: LUncov, LAnnotate and LReplay)
has been (re-)released on
[
Frama-C's public Gitlab
](
https://git.frama-c.com/pub/ltest
)
,
and as 3 opam packages:
[
frama-c-luncov
](
https://opam.ocaml.org/packages/frama-c-luncov/
)
,
[
frama-c-lannotate
](
https://opam.ocaml.org/packages/frama-c-lannotate/
)
,
and
[
lreplay
](
https://opam.ocaml.org/packages/lreplay/
)
.
These plugins help measure test coverage based on
*hyperlabels*
.
Details about them are published
[
here
](
http://sebastien.bardin.free.fr/final-SCP-2021.pdf
)
and
[
here
](
http://sebastien.bardin.free.fr/2017-icst-tool.pdf
)
(you can also see the
[
LTest plugin page on the Frama-C website
](
https://www.frama-c.com/fc-plugins/ltest.html
)
).
Note that these plugins do not help generating test cases;
for that, you may want to use
[
PathCrawler
](
https://www.frama-c.com/fc-plugins/pathcrawler.html
)
(not open-source).
## A bit of history
The LTest plugin is not new: it
[
has been released several years ago
](
https://micdel.fr/ltest.html
)
,
as part of Mickaël Delahaye's PhD. However, that version (compatible with
a patched version of Frama-C Neon) has aged a bit, making it hard for users
to get it working with recent Frama-C versions. Other releases were made
on
[
Github
](
https://github.com/ltest-dev/LTest
)
, usually related to published
papers, but once again, their maintenance was sporadic.
This opam release, plus the code being kept closer to Frama-C's development
version in Gitlab, should help keep these plug-ins relevant. Note that the
released version is numbered 0.1, which indicates that they are still in an
experimental stage; industrial users should contact the Frama-C team for
details about their maturity.
You may also have noticed: why is the opam package for LReplay named
`lreplay`
and not
`frama-c-lreplay`
? The simple reason is that, unlike the
others, it is not a Frama-C plug-in
*per se*
, but an independent tool
(it even has its own Dune build file) that can be used with or without
Frama-C. It turns out that its defaults are mostly tuned for using it in
conjunction with
[
PathCrawler
](
https://www.frama-c.com/fc-plugins/pathcrawler.html
)
,
but it can be configured for use with other test generators.
Loading