From 660250dcf775c6fab13a2ecdc6666cb87687907b Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 4 Apr 2016 05:36:31 -0700 Subject: [PATCH] move Dom.JoinState to its own file Summary:public Will be needed later to avoid circular dependencies between dom.ml and upcoming numericalDomain.ml. Reviewed By: jberdine Differential Revision: D3126697 fb-gh-sync-id: 678d49f fbshipit-source-id: 678d49f --- infer/src/backend/dom.ml | 17 ----------------- infer/src/backend/joinState.ml | 21 +++++++++++++++++++++ infer/src/backend/joinState.mli | 17 +++++++++++++++++ 3 files changed, 38 insertions(+), 17 deletions(-) create mode 100644 infer/src/backend/joinState.ml create mode 100644 infer/src/backend/joinState.mli diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index abf16f6d8..28eb024e9 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -16,23 +16,6 @@ module F = Format let (++) = Sil.Int.add let (--) = Sil.Int.sub -(** {2 Object representing the status of the join operation} *) - -module JoinState : sig - - type mode = Pre | Post - val get_footprint : unit -> bool - val set_footprint : bool -> unit - -end = struct - - type mode = Pre | Post - let footprint = ref false (* set to true when we are doing join of footprints *) - let get_footprint () = !footprint - let set_footprint b = footprint := b - -end - (** {2 Utility functions for ids} *) let can_rename id = diff --git a/infer/src/backend/joinState.ml b/infer/src/backend/joinState.ml new file mode 100644 index 000000000..d3ce0834b --- /dev/null +++ b/infer/src/backend/joinState.ml @@ -0,0 +1,21 @@ +(* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +(** Object representing the status of the join operation *) + +type mode = + | Pre + | Post + +(** set to true when we are doing join of footprints *) +let footprint = ref false + +let get_footprint () = !footprint + +let set_footprint b = footprint := b diff --git a/infer/src/backend/joinState.mli b/infer/src/backend/joinState.mli new file mode 100644 index 000000000..f74e2fe64 --- /dev/null +++ b/infer/src/backend/joinState.mli @@ -0,0 +1,17 @@ +(* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +(** Object representing the status of the join operation *) + +type mode = + | Pre + | Post + +val get_footprint : unit -> bool +val set_footprint : bool -> unit