From c1d603f6b27427b3cbbfb6401829d829c4094de0 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 29 Apr 2020 02:58:40 -0700 Subject: [PATCH] add .mli to Scheduler Summary: We like .mli files. Reviewed By: ngorogiannis Differential Revision: D21257473 fbshipit-source-id: 13c3faa77 --- infer/src/absint/Scheduler.ml | 9 --------- infer/src/absint/Scheduler.mli | 27 +++++++++++++++++++++++++++ 2 files changed, 27 insertions(+), 9 deletions(-) create mode 100644 infer/src/absint/Scheduler.mli diff --git a/infer/src/absint/Scheduler.ml b/infer/src/absint/Scheduler.ml index c4cf0ebaf..83902ae94 100644 --- a/infer/src/absint/Scheduler.ml +++ b/infer/src/absint/Scheduler.ml @@ -13,21 +13,12 @@ module type S = sig type t val schedule_succs : t -> CFG.Node.t -> t - (** schedule the successors of [node] *) val pop : t -> (CFG.Node.t * CFG.Node.id list * t) option - (** remove and return the node with the highest priority, the ids of its visited predecessors, and - the new schedule *) val empty : CFG.t -> t end -module type Make = functor (CFG : ProcCfg.S) -> sig - include S with module CFG = CFG -end - -(** simple scheduler that visits CFG nodes in reverse postorder. fast/precise for straightline code - and conditionals; not as good for loops (may visit nodes after a loop multiple times). *) module ReversePostorder (CFG : ProcCfg.S) = struct module CFG = CFG module M = CFG.Node.IdMap diff --git a/infer/src/absint/Scheduler.mli b/infer/src/absint/Scheduler.mli new file mode 100644 index 000000000..47cf83861 --- /dev/null +++ b/infer/src/absint/Scheduler.mli @@ -0,0 +1,27 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +module type S = sig + module CFG : ProcCfg.S + + type t + + val schedule_succs : t -> CFG.Node.t -> t + (** schedule the successors of [node] *) + + val pop : t -> (CFG.Node.t * CFG.Node.id list * t) option + (** remove and return the node with the highest priority, the ids of its visited predecessors, and + the new schedule *) + + val empty : CFG.t -> t +end + +(** simple scheduler that visits CFG nodes in reverse postorder. fast/precise for straightline code + and conditionals; not as good for loops (may visit nodes after a loop multiple times). *) +module ReversePostorder (CFG : ProcCfg.S) : S with module CFG = CFG