From 084fd9301be42b5a24980b8b6abc2bb46c399fe1 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 19 Dec 2016 10:28:47 -0800 Subject: [PATCH] [absint] Fix capitalization of abstractInterpreter.mli and reconcile with the source file Summary: Good catch from https://github.com/facebook/infer/issues/539#issuecomment-267988365. Reviewed By: jvillard Differential Revision: D4346497 fbshipit-source-id: 6c08c6b --- .../{abstractDomain.ml => AbstractDomain.ml} | 0 ...ctInterpreter.ml => AbstractInterpreter.ml} | 18 ++++++------------ infer/src/checkers/AbstractInterpreter.mli | 2 +- 3 files changed, 7 insertions(+), 13 deletions(-) rename infer/src/checkers/{abstractDomain.ml => AbstractDomain.ml} (100%) rename infer/src/checkers/{abstractInterpreter.ml => AbstractInterpreter.ml} (93%) diff --git a/infer/src/checkers/abstractDomain.ml b/infer/src/checkers/AbstractDomain.ml similarity index 100% rename from infer/src/checkers/abstractDomain.ml rename to infer/src/checkers/AbstractDomain.ml diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/AbstractInterpreter.ml similarity index 93% rename from infer/src/checkers/abstractInterpreter.ml rename to infer/src/checkers/AbstractInterpreter.ml index a89304346..900bceba4 100644 --- a/infer/src/checkers/abstractInterpreter.ml +++ b/infer/src/checkers/AbstractInterpreter.ml @@ -15,27 +15,21 @@ type 'a state = { pre: 'a; post: 'a; visit_count: int; } module type S = sig module TransferFunctions : TransferFunctions.S + module InvariantMap : Caml.Map.S with type key = TransferFunctions.CFG.id - module Interprocedural - (Summary : Summary.S with type summary = TransferFunctions.Domain.astate) : - sig - - (** compute and return the summary for the given procedure and store it on disk using - [compute_post]. *) - val compute_and_store_post : - compute_post: ('a ProcData.t -> Summary.summary option) -> - make_extras : (Procdesc.t -> 'a) -> - Callbacks.proc_callback_args -> - Summary.summary option - end type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t val compute_post : TransferFunctions.extras ProcData.t -> TransferFunctions.Domain.astate option + val exec_cfg : TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t -> invariant_map + val exec_pdesc : TransferFunctions.extras ProcData.t -> invariant_map + val extract_post : InvariantMap.key -> 'a state InvariantMap.t -> 'a option + val extract_pre : InvariantMap.key -> 'a state InvariantMap.t -> 'a option + val extract_state : InvariantMap.key -> 'a InvariantMap.t -> 'a option end diff --git a/infer/src/checkers/AbstractInterpreter.mli b/infer/src/checkers/AbstractInterpreter.mli index a72d497c3..2b49eb8d3 100644 --- a/infer/src/checkers/AbstractInterpreter.mli +++ b/infer/src/checkers/AbstractInterpreter.mli @@ -15,7 +15,7 @@ type 'a state = { pre: 'a; post: 'a; visit_count: int; } module type S = sig module TransferFunctions : TransferFunctions.S - module InvariantMap : Map.S with type key = TransferFunctions.CFG.id + module InvariantMap : Caml.Map.S with type key = TransferFunctions.CFG.id (** invariant map from node id -> state representing postcondition for node id *) type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t