From d54cb4800dae4d1a32c9e36bcfaa828413991362 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 22 Jan 2021 08:43:56 +0100
Subject: [PATCH] [wp] please the linter
---
headers/header_spec.txt | 2 ++
src/plugins/wp/cfgGenerator.ml | 4 ++--
2 files changed, 4 insertions(+), 2 deletions(-)
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 7525ffd94ff..7698e1df5e9 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1680,6 +1680,8 @@ src/plugins/wp/cfgCalculus.ml: CEA_WP
src/plugins/wp/cfgCalculus.mli: CEA_WP
src/plugins/wp/cfgDump.ml: CEA_WP
src/plugins/wp/cfgDump.mli: CEA_WP
+src/plugins/wp/cfgGenerator.ml: CEA_WP
+src/plugins/wp/cfgGenerator.mli: CEA_WP
src/plugins/wp/cfgInit.ml: CEA_WP
src/plugins/wp/cfgInit.mli: CEA_WP
src/plugins/wp/cfgWP.ml: CEA_WP
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index e9cd98fec7e..2fe63d14871 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -141,8 +141,8 @@ struct
begin fun () ->
LogicUsage.iter_lemmas VCG.register_lemma ;
List.iter (fun l ->
- let wpo = VCG.compile_lemma l in
- collection := Bag.add wpo !collection
+ let wpo = VCG.compile_lemma l in
+ collection := Bag.add wpo !collection
) task.lemmas ;
end () ;
List.iter
--
GitLab