From 8ccf26816f3ebd23900fd655d703d04dba4da957 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 28 Jan 2021 10:27:52 +0100
Subject: [PATCH] [wp] small fix after rebase
---
src/kernel_services/analysis/interpreted_automata.ml | 2 +-
src/plugins/wp/cfgGenerator.ml | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index 2810d1add1c..11aeaa41e39 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -305,7 +305,7 @@ let build_automaton ~annotations kf =
in
let build_stmt_transition src dest stmt succ transition =
ignore (build_stmt_next src dest stmt succ transition) in
-
+
let rec do_list do_one control labels = function
| [] -> assert false
| stmt :: [] -> do_one control labels stmt
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index 5827e2b3b24..19c83200459 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -65,7 +65,7 @@ let apply task ~kf ?bhvs ?prop () =
List.iter (fun bhv ->
task.modes <- { kf ; bhv } :: task.modes
) bhvs ;
- Extlib.may (fun ip -> task.props <- `PropId ip) prop ;
+ Option.iter (fun ip -> task.props <- `PropId ip) prop ;
end
let notyet prop =
--
GitLab