From ffb202d89972a1c0e3d2edc03e9446cb386039d4 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 19 Aug 2021 15:00:59 +0200
Subject: [PATCH] Avoid issues with Landmarks' PPX and constructors inside
methods
---
src/plugins/dive/build.ml | 2 +-
src/plugins/wp/TacInduction.ml | 2 +-
src/plugins/wp/TacSequence.ml | 2 +-
3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 5ed33280abb..6a08979f28d 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -47,7 +47,7 @@ struct
let visitor f =
object
inherit Visitor.frama_c_inplace
- method! vlval lval = f lval; SkipChildren
+ method! vlval lval = f lval; Cil.SkipChildren
end
let from_exp f exp =
diff --git a/src/plugins/wp/TacInduction.ml b/src/plugins/wp/TacInduction.ml
index 982d6e13094..4098efd7c3a 100644
--- a/src/plugins/wp/TacInduction.ml
+++ b/src/plugins/wp/TacInduction.ml
@@ -108,7 +108,7 @@ class induction =
let value = Tactical.selected s in
if F.is_int value then
match self#get_base () with
- | Some base -> Applicable(process value base)
+ | Some base -> Tactical.Applicable(process value base)
| None -> Not_configured
else Not_applicable
diff --git a/src/plugins/wp/TacSequence.ml b/src/plugins/wp/TacSequence.ml
index 8a0dbdeea4c..3671cd67b73 100644
--- a/src/plugins/wp/TacSequence.ml
+++ b/src/plugins/wp/TacSequence.ml
@@ -59,7 +59,7 @@ class sequence =
| Fun(f,[a;n]) when f == Vlist.f_repeat ->
let result = F.typeof value in
let at = Tactical.at s in
- Applicable
+ Tactical.Applicable
begin
match self#get_field vmode with
| `Sum ->
--
GitLab