From 2baab0d3fedb2f2d4a3dc46a75d69f7d2c13123b Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 21 Feb 2019 10:19:06 +0100
Subject: [PATCH] [rte] remove 'open Flags'
---
src/plugins/rte/register.ml | 6 ++----
src/plugins/rte/visit.ml | 37 ++++++++++++++++++++-----------------
2 files changed, 22 insertions(+), 21 deletions(-)
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index 87386ea7f8b..ab0d3111c0a 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -24,14 +24,12 @@
(* dedicated computations *)
(* -------------------------------------------------------------------------- *)
-open Flags
-
(* annotate for all rte + unsigned overflows (which are not rte), for a given
function *)
let do_all_rte kf =
let flags =
{ Flags.all with
- signed_downcast = false;
+ Flags.signed_downcast = false;
unsigned_downcast = false; }
in
Visit.annotate ~flags kf
@@ -41,7 +39,7 @@ let do_all_rte kf =
let do_rte kf =
let flags =
{ Flags.all with
- unsigned_overflow = false;
+ Flags.unsigned_overflow = false;
signed_downcast = false;
unsigned_downcast = false; }
in
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 9bd7ee4f39b..0a7c6fa81ba 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -24,7 +24,6 @@
open Cil_types
open Cil_datatype
-open Flags
(* AST inplace visitor for runtime annotation generation *)
@@ -52,49 +51,52 @@ class annot_visitor kf flags on_alarm = object (self)
r
method private do_initialized () =
- flags.initialized && not (Generator.Initialized.is_computed kf)
+ flags.Flags.initialized && not (Generator.Initialized.is_computed kf)
method private do_mem_access () =
- flags.mem_access && not (Generator.Mem_access.is_computed kf)
+ flags.Flags.mem_access && not (Generator.Mem_access.is_computed kf)
method private do_div_mod () =
- flags.div_mod && not (Generator.Div_mod.is_computed kf)
+ flags.Flags.div_mod && not (Generator.Div_mod.is_computed kf)
method private do_shift () =
- flags.shift && not (Generator.Shift.is_computed kf)
+ flags.Flags.shift && not (Generator.Shift.is_computed kf)
method private do_left_shift_negative () =
- flags.left_shift_negative
+ flags.Flags.left_shift_negative
&& not (Generator.Left_shift_negative.is_computed kf)
method private do_right_shift_negative () =
- flags.right_shift_negative
+ flags.Flags.right_shift_negative
&& not (Generator.Right_shift_negative.is_computed kf)
method private do_signed_overflow () =
- flags.signed_overflow && not (Generator.Signed_overflow.is_computed kf)
+ flags.Flags.signed_overflow
+ && not (Generator.Signed_overflow.is_computed kf)
method private do_unsigned_overflow () =
- flags.unsigned_overflow && not (Generator.Unsigned_overflow.is_computed kf)
+ flags.Flags.unsigned_overflow
+ && not (Generator.Unsigned_overflow.is_computed kf)
method private do_signed_downcast () =
- flags.signed_downcast && not (Generator.Signed_downcast.is_computed kf)
+ flags.Flags.signed_downcast
+ && not (Generator.Signed_downcast.is_computed kf)
method private do_unsigned_downcast () =
- flags.unsigned_downcast &&
- not (Generator.Unsigned_downcast.is_computed kf)
+ flags.Flags.unsigned_downcast
+ && not (Generator.Unsigned_downcast.is_computed kf)
method private do_float_to_int () =
- flags.float_to_int && not (Generator.Float_to_int.is_computed kf)
+ flags.Flags.float_to_int && not (Generator.Float_to_int.is_computed kf)
method private do_finite_float () =
- flags.finite_float && not (Generator.Finite_float.is_computed kf)
+ flags.Flags.finite_float && not (Generator.Finite_float.is_computed kf)
method private do_pointer_call () =
- flags.pointer_call && not (Generator.Pointer_call.is_computed kf)
+ flags.Flags.pointer_call && not (Generator.Pointer_call.is_computed kf)
method private do_bool_value () =
- flags.bool_value && not (Generator.Bool_value.is_computed kf)
+ flags.Flags.bool_value && not (Generator.Bool_value.is_computed kf)
method private queue_stmt_spec spec =
let stmt = Extlib.the (self#current_stmt) in
@@ -108,7 +110,7 @@ class annot_visitor kf flags on_alarm = object (self)
fun fgen ->
let stmt = Extlib.the (self#current_stmt) in
let on_alarm ~invalid a = on_alarm stmt ~invalid a in
- fgen ~remove_trivial:flags.remove_trivial ~on_alarm
+ fgen ~remove_trivial:flags.Flags.remove_trivial ~on_alarm
method! vstmt s = match s.skind with
| UnspecifiedSequence l ->
@@ -430,6 +432,7 @@ let annotate ?flags kf =
(* Strict version of ||, because [comp] has side-effects *)
let (|||) a b = a || b in
let open Generator in
+ let open Flags in
if comp Initialized.accessor flags.initialized |||
comp Mem_access.accessor flags.mem_access |||
comp Pointer_call.accessor flags.pointer_call |||
--
GitLab