The R13B03 release.OTP_R13B03

1 files changed, 540 insertions, 0 deletions

diff --git a/lib/dialyzer/src/dialyzer_succ_typings.erl b/lib/dialyzer/src/dialyzer_succ_typings.erl
new file mode 100644
index 0000000000..dd8480f1f2
--- /dev/null
+++ b/lib/dialyzer/src/dialyzer_succ_typings.erl
@@ -0,0 +1,540 @@
+%% -*- erlang-indent-level: 2 -*-
+%%-----------------------------------------------------------------------
+%% %CopyrightBegin%
+%% 
+%% Copyright Ericsson AB 2006-2009. All Rights Reserved.
+%% 
+%% The contents of this file are subject to the Erlang Public License,
+%% Version 1.1, (the "License"); you may not use this file except in
+%% compliance with the License. You should have received a copy of the
+%% Erlang Public License along with this software. If not, it can be
+%% retrieved online at http://www.erlang.org/.
+%% 
+%% Software distributed under the License is distributed on an "AS IS"
+%% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See
+%% the License for the specific language governing rights and limitations
+%% under the License.
+%% 
+%% %CopyrightEnd%
+%%
+
+%%%-------------------------------------------------------------------
+%%% File    : dialyzer_succ_typings.erl
+%%% Author  : Tobias Lindahl <[email protected]>
+%%% Description : 
+%%%
+%%% Created : 11 Sep 2006 by Tobias Lindahl <[email protected]>
+%%%-------------------------------------------------------------------
+-module(dialyzer_succ_typings).
+
+-export([analyze_callgraph/3, 
+	 analyze_callgraph/4,
+	 get_warnings/6]).
+
+%% These are only intended as debug functions.
+-export([doit/1,
+	 get_top_level_signatures/3]).
+
+%%-define(DEBUG, true).
+%%-define(DEBUG_PP, true).
+
+-ifdef(DEBUG).
+-define(debug(X__, Y__), io:format(X__, Y__)).
+-else.
+-define(debug(X__, Y__), ok).
+-endif.
+
+-define(TYPE_LIMIT, 4).
+
+%%--------------------------------------------------------------------
+
+-include("dialyzer.hrl").
+
+%%--------------------------------------------------------------------
+%% State record -- local to this module
+
+-type parent() :: 'none' | pid().
+
+-record(st, {callgraph      :: dialyzer_callgraph:callgraph(),
+	     codeserver     :: dialyzer_codeserver:codeserver(),
+	     no_warn_unused :: set(),
+	     parent = none  :: parent(),
+	     plt            :: dialyzer_plt:plt()}).
+
+%%--------------------------------------------------------------------
+
+-spec analyze_callgraph(dialyzer_callgraph:callgraph(), dialyzer_plt:plt(),
+			dialyzer_codeserver:codeserver()) ->
+	 dialyzer_plt:plt().
+
+analyze_callgraph(Callgraph, Plt, Codeserver) ->
+  analyze_callgraph(Callgraph, Plt, Codeserver, none).
+
+-spec analyze_callgraph(dialyzer_callgraph:callgraph(), dialyzer_plt:plt(),
+			dialyzer_codeserver:codeserver(), parent()) ->
+         dialyzer_plt:plt().
+
+analyze_callgraph(Callgraph, Plt, Codeserver, Parent) ->
+  State = #st{callgraph = Callgraph, plt = Plt, 
+	      codeserver = Codeserver, parent = Parent},
+  NewState = get_refined_success_typings(State),
+  NewState#st.plt.
+
+%%--------------------------------------------------------------------
+
+get_refined_success_typings(State) ->
+  case find_succ_typings(State) of
+    {fixpoint, State1} -> State1;
+    {not_fixpoint, NotFixpoint1, State1} ->
+      Callgraph = State1#st.callgraph,
+      NotFixpoint2 = [lookup_name(F, Callgraph) || F <- NotFixpoint1],
+      ModulePostorder = 
+	dialyzer_callgraph:module_postorder_from_funs(NotFixpoint2, Callgraph),
+      case refine_succ_typings(ModulePostorder, State1) of
+	{fixpoint, State2} ->
+	  State2;
+	{not_fixpoint, NotFixpoint3, State2} ->
+	  Callgraph1 = State2#st.callgraph,
+	  %% Need to reset the callgraph.
+	  NotFixpoint4 = [lookup_name(F, Callgraph1) || F <- NotFixpoint3],
+	  Callgraph2 = dialyzer_callgraph:reset_from_funs(NotFixpoint4, 
+							  Callgraph1),
+	  get_refined_success_typings(State2#st{callgraph = Callgraph2})
+      end
+  end.
+
+-type doc_plt() :: 'undefined' | dialyzer_plt:plt().
+-spec get_warnings(dialyzer_callgraph:callgraph(), dialyzer_plt:plt(),
+		   doc_plt(), dialyzer_codeserver:codeserver(), set(),
+		   pid()) -> 
+	 {[dial_warning()], dialyzer_plt:plt(), doc_plt()}.
+
+get_warnings(Callgraph, Plt, DocPlt, Codeserver, NoWarnUnused, Parent) ->
+  InitState = #st{callgraph = Callgraph, codeserver = Codeserver,
+		  no_warn_unused = NoWarnUnused, parent = Parent, plt = Plt},
+  NewState = get_refined_success_typings(InitState),
+  Mods = dialyzer_callgraph:modules(NewState#st.callgraph),
+  CWarns = dialyzer_contracts:get_invalid_contract_warnings(Mods, Codeserver,
+							    NewState#st.plt),
+  get_warnings_from_modules(Mods, NewState, DocPlt, CWarns).
+
+get_warnings_from_modules([M|Ms], State, DocPlt, Acc) when is_atom(M) ->
+  send_log(State#st.parent, io_lib:format("Getting warnings for ~w\n", [M])),
+  #st{callgraph = Callgraph, codeserver = Codeserver,
+      no_warn_unused = NoWarnUnused, plt = Plt} = State,
+  ModCode = dialyzer_codeserver:lookup_mod_code(M, Codeserver),
+  Records = dialyzer_codeserver:lookup_mod_records(M, Codeserver),
+  Contracts = dialyzer_codeserver:lookup_mod_contracts(M, Codeserver),
+  AllFuns = collect_fun_info([ModCode]),
+  %% Check if there are contracts for functions that do not exist
+  Warnings1 = 
+    dialyzer_contracts:contracts_without_fun(Contracts, AllFuns, Callgraph),
+  {Warnings2, FunTypes, RaceCode, PublicTables, NamedTables} =
+    dialyzer_dataflow:get_warnings(ModCode, Plt, Callgraph, Records, NoWarnUnused),
+  NewDocPlt = insert_into_doc_plt(FunTypes, Callgraph, DocPlt),
+  NewCallgraph =
+    dialyzer_callgraph:renew_race_info(Callgraph, RaceCode, PublicTables,
+                                       NamedTables),
+  State1 = st__renew_state_calls(NewCallgraph, State),
+  get_warnings_from_modules(Ms, State1, NewDocPlt, [Warnings1,Warnings2|Acc]);
+get_warnings_from_modules([], #st{plt = Plt}, DocPlt, Acc) ->
+  {lists:flatten(Acc), Plt, DocPlt}.
+
+refine_succ_typings(ModulePostorder, State) ->
+  ?debug("Module postorder: ~p\n", [ModulePostorder]),
+  refine_succ_typings(ModulePostorder, State, []).
+
+refine_succ_typings([SCC|SCCs], State, Fixpoint) ->
+  Msg = io_lib:format("Dataflow of one SCC: ~w\n", [SCC]),
+  send_log(State#st.parent, Msg),
+  ?debug("~s\n", [Msg]),
+  {NewState, FixpointFromScc} =
+    case SCC of
+      [M] -> refine_one_module(M, State);
+      [_|_] -> refine_one_scc(SCC, State)
+    end,
+  NewFixpoint = ordsets:union(Fixpoint, FixpointFromScc),
+  refine_succ_typings(SCCs, NewState, NewFixpoint);
+refine_succ_typings([], State, Fixpoint) ->
+  case Fixpoint =:= [] of
+    true -> {fixpoint, State};
+    false -> {not_fixpoint, Fixpoint, State}
+  end.
+
+-spec refine_one_module(module(), #st{}) -> {#st{}, [label()]}. % ordset
+
+refine_one_module(M, State) ->
+  #st{callgraph = Callgraph, codeserver = CodeServer, plt = PLT} = State,
+  ModCode = dialyzer_codeserver:lookup_mod_code(M, CodeServer),
+  AllFuns = collect_fun_info([ModCode]),
+  FunTypes = get_fun_types_from_plt(AllFuns, State),
+  Records = dialyzer_codeserver:lookup_mod_records(M, CodeServer),
+  {NewFunTypes, RaceCode, PublicTables, NamedTables} =
+    dialyzer_dataflow:get_fun_types(ModCode, PLT, Callgraph, Records),
+  NewCallgraph =
+    dialyzer_callgraph:renew_race_info(Callgraph, RaceCode, PublicTables,
+                                       NamedTables),
+  case reached_fixpoint(FunTypes, NewFunTypes) of
+    true ->
+      State1 = st__renew_state_calls(NewCallgraph, State),
+      {State1, ordsets:new()};
+    {false, NotFixpoint} ->
+      ?debug("Not fixpoint\n", []),
+      NewState = insert_into_plt(dict:from_list(NotFixpoint), State),
+      NewState1 = st__renew_state_calls(NewCallgraph, NewState),
+      {NewState1, ordsets:from_list([FunLbl || {FunLbl,_Type} <- NotFixpoint])}
+  end.
+
+st__renew_state_calls(Callgraph, State) ->
+  State#st{callgraph = Callgraph}.
+
+refine_one_scc(SCC, State) ->
+  refine_one_scc(SCC, State, []).
+
+refine_one_scc(SCC, State, AccFixpoint) ->
+  {NewState, FixpointFromScc} = refine_mods_in_scc(SCC, State, []),
+  case FixpointFromScc =:= [] of
+    true -> {NewState, AccFixpoint};
+    false ->
+      NewAccFixpoint = ordsets:union(AccFixpoint, FixpointFromScc),
+      refine_one_scc(SCC, NewState, NewAccFixpoint)
+  end.
+
+refine_mods_in_scc([Mod|Mods], State, Fixpoint) ->
+  {NewState, FixpointFromModule} = refine_one_module(Mod, State),
+  NewFixpoint = ordsets:union(FixpointFromModule, Fixpoint),
+  refine_mods_in_scc(Mods, NewState, NewFixpoint);
+refine_mods_in_scc([], State, Fixpoint) ->
+  {State, Fixpoint}.
+
+reached_fixpoint(OldTypes, NewTypes) ->
+  reached_fixpoint(OldTypes, NewTypes, false).
+
+reached_fixpoint_strict(OldTypes, NewTypes) ->
+  case reached_fixpoint(OldTypes, NewTypes, true) of
+    true -> true;
+    {false, _} -> false
+  end.
+
+reached_fixpoint(OldTypes0, NewTypes0, Strict) ->
+  MapFun = fun(_Key, Type) ->
+	       case is_failed_or_not_called_fun(Type) of
+		 true -> failed_fun;
+		 false -> erl_types:t_limit(Type, ?TYPE_LIMIT)
+	       end
+	   end,
+  OldTypes = dict:map(MapFun, OldTypes0),
+  NewTypes = dict:map(MapFun, NewTypes0),
+  compare_types(OldTypes, NewTypes, Strict).
+
+is_failed_or_not_called_fun(Type) ->
+  erl_types:any_none([erl_types:t_fun_range(Type)|erl_types:t_fun_args(Type)]).
+
+compare_types(Dict1, Dict2, Strict) ->  
+  List1 = lists:keysort(1, dict:to_list(Dict1)),
+  List2 = lists:keysort(1, dict:to_list(Dict2)),
+  compare_types_1(List1, List2, Strict, []).
+
+compare_types_1([{X, _Type1}|Left1], [{X, failed_fun}|Left2], 
+		Strict, NotFixpoint) ->
+  compare_types_1(Left1, Left2, Strict, NotFixpoint);
+compare_types_1([{X, failed_fun}|Left1], [{X, _Type2}|Left2], 
+		Strict, NotFixpoint) ->
+  compare_types_1(Left1, Left2, Strict, NotFixpoint);
+compare_types_1([{X, Type1}|Left1], [{X, Type2}|Left2], Strict, NotFixpoint) ->
+  Res = case Strict of
+	  true -> erl_types:t_is_equal(Type1, Type2);
+	  false -> erl_types:t_is_subtype(Type1, Type2)
+	end,
+  case Res of
+    true -> compare_types_1(Left1, Left2, Strict, NotFixpoint);
+    false -> 
+      ?debug("Failed fixpoint for ~w: ~s =/= ~s\n",
+	     [X, erl_types:t_to_string(Type1), erl_types:t_to_string(Type2)]),
+      compare_types_1(Left1, Left2, Strict, [{X, Type2}|NotFixpoint])
+  end;
+compare_types_1([_|Left1], List2, Strict, NotFixpoint) ->
+  %% If the function was not called.
+  compare_types_1(Left1, List2, Strict, NotFixpoint);
+compare_types_1([], [], _Strict, NotFixpoint) ->
+  case NotFixpoint =:= [] of
+    true -> true;
+    false -> {false, NotFixpoint}
+  end.
+
+find_succ_typings(State) ->
+  find_succ_typings(State, []).
+
+find_succ_typings(#st{callgraph = Callgraph, parent = Parent} = State,
+		  NotFixpoint) ->
+  case dialyzer_callgraph:take_scc(Callgraph) of
+    {ok, SCC, NewCallgraph} ->
+      Msg = io_lib:format("Typesig analysis for SCC: ~w\n", [format_scc(SCC)]),
+      ?debug("~s", [Msg]),
+      send_log(Parent, Msg),
+      {NewState, NewNotFixpoint1} =
+	analyze_scc(SCC, State#st{callgraph = NewCallgraph}),
+      NewNotFixpoint2 = ordsets:union(NewNotFixpoint1, NotFixpoint),
+      find_succ_typings(NewState, NewNotFixpoint2);
+    none ->
+      ?debug("==================== Typesig done ====================\n\n", []),
+      case NotFixpoint =:= [] of
+	true -> {fixpoint, State};
+	false -> {not_fixpoint, NotFixpoint, State}
+      end
+  end.
+
+analyze_scc(SCC, #st{codeserver = Codeserver} = State) ->
+  SCC_Info = [{MFA, 
+	       dialyzer_codeserver:lookup_mfa_code(MFA, Codeserver),
+	       dialyzer_codeserver:lookup_mod_records(M, Codeserver)}
+	      || {M, _, _} = MFA <- SCC],
+  Contracts1 = [{MFA, dialyzer_codeserver:lookup_mfa_contract(MFA, Codeserver)}
+		|| {_, _, _} = MFA <- SCC],
+  Contracts2 = [{MFA, Contract} || {MFA, {ok, Contract}} <- Contracts1],
+  Contracts3 = orddict:from_list(Contracts2),
+  {SuccTypes, PltContracts, NotFixpoint} = 
+    find_succ_types_for_scc(SCC_Info, Contracts3, State),
+  State1 = insert_into_plt(SuccTypes, State),
+  ContrPlt = dialyzer_plt:insert_contract_list(State1#st.plt, PltContracts),
+  {State1#st{plt = ContrPlt}, NotFixpoint}.
+
+find_succ_types_for_scc(SCC_Info, Contracts, 
+			#st{codeserver = Codeserver, 
+			    callgraph = Callgraph, plt = Plt} = State) ->
+  %% Assume that the PLT contains the current propagated types
+  AllFuns = collect_fun_info([Fun || {_MFA, {_Var, Fun}, _Rec} <- SCC_Info]),
+  PropTypes = get_fun_types_from_plt(AllFuns, State),
+  MFAs = [MFA || {MFA, {_Var, _Fun}, _Rec} <- SCC_Info],
+  NextLabel = dialyzer_codeserver:get_next_core_label(Codeserver),
+  Plt1 = dialyzer_plt:delete_contract_list(Plt, MFAs),
+  FunTypes = dialyzer_typesig:analyze_scc(SCC_Info, NextLabel, 
+					  Callgraph, Plt1, PropTypes),
+  AllFunSet = sets:from_list([X || {X, _} <- AllFuns]),
+  FilteredFunTypes = dict:filter(fun(X, _) ->
+				      sets:is_element(X, AllFunSet) 
+				  end, FunTypes),
+  %% Check contracts
+  PltContracts = dialyzer_contracts:check_contracts(Contracts, Callgraph, 
+						    FilteredFunTypes),
+  ContractFixpoint =
+    lists:all(fun({MFA, _C}) ->
+		  %% Check the non-deleted PLT
+		  case dialyzer_plt:lookup_contract(Plt, MFA) of
+		    none -> false;
+		    {value, _} -> true
+		  end
+	      end, PltContracts),
+  case (ContractFixpoint andalso 
+	reached_fixpoint_strict(PropTypes, FilteredFunTypes)) of
+    true ->
+      {FilteredFunTypes, PltContracts, []};
+    false ->
+      ?debug("Not fixpoint for: ~w\n", [AllFuns]),
+      {FilteredFunTypes, PltContracts,
+       ordsets:from_list([Fun || {Fun, _Arity} <- AllFuns])}
+  end.
+
+get_fun_types_from_plt(FunList, State) ->
+  get_fun_types_from_plt(FunList, State, dict:new()).
+
+get_fun_types_from_plt([{FunLabel, Arity}|Left], State, Map) ->
+  Type = lookup_fun_type(FunLabel, Arity, State),
+  get_fun_types_from_plt(Left, State, dict:store(FunLabel, Type, Map));
+get_fun_types_from_plt([], _State, Map) ->
+  Map.
+
+collect_fun_info(Trees) ->
+  collect_fun_info(Trees, []).
+
+collect_fun_info([Tree|Trees], List) ->
+  Fun = fun(SubTree, Acc) ->
+	    case cerl:is_c_fun(SubTree) of
+	      true ->
+		[{cerl_trees:get_label(SubTree), cerl:fun_arity(SubTree)}|Acc];
+	      false -> Acc
+	    end
+	end,
+  collect_fun_info(Trees, cerl_trees:fold(Fun, List, Tree));
+collect_fun_info([], List) ->
+  List.
+
+lookup_fun_type(Label, Arity, #st{callgraph = Callgraph, plt = Plt}) ->
+  ID = lookup_name(Label, Callgraph),
+  case dialyzer_plt:lookup(Plt, ID) of
+    none -> erl_types:t_fun(Arity, erl_types:t_any());
+    {value, {RetT, ArgT}} -> erl_types:t_fun(ArgT, RetT)
+  end.
+
+insert_into_doc_plt(_FunTypes, _Callgraph, undefined) ->
+  undefined;
+insert_into_doc_plt(FunTypes, Callgraph, DocPlt) ->
+  SuccTypes = format_succ_types(FunTypes, Callgraph),
+  dialyzer_plt:insert_list(DocPlt, SuccTypes).
+
+insert_into_plt(SuccTypes0, #st{callgraph = Callgraph, plt = Plt} = State) ->
+  SuccTypes = format_succ_types(SuccTypes0, Callgraph),
+  debug_pp_succ_typings(SuccTypes),
+  State#st{plt = dialyzer_plt:insert_list(Plt, SuccTypes)}.
+
+format_succ_types(SuccTypes, Callgraph) ->
+  format_succ_types(dict:to_list(SuccTypes), Callgraph, []).
+
+format_succ_types([{Label, Type0}|Left], Callgraph, Acc) ->
+  Type = erl_types:t_limit(Type0, ?TYPE_LIMIT+1),
+  Id = lookup_name(Label, Callgraph),
+  NewTuple = {Id, {erl_types:t_fun_range(Type), erl_types:t_fun_args(Type)}},
+  format_succ_types(Left, Callgraph, [NewTuple|Acc]);
+format_succ_types([], _Callgraph, Acc) ->
+  Acc.
+
+-ifdef(DEBUG).
+debug_pp_succ_typings(SuccTypes) ->
+  ?debug("Succ typings:\n", []),
+  [?debug("  ~w :: ~s\n", 
+	  [MFA, erl_types:t_to_string(erl_types:t_fun(ArgT, RetT))])
+   || {MFA, {RetT, ArgT}} <- SuccTypes],
+  ?debug("Contracts:\n", []),
+  [?debug("  ~w :: ~s\n", 
+	  [MFA, erl_types:t_to_string(erl_types:t_fun(ArgT, RetFun(ArgT)))])
+   || {MFA, {contract, RetFun, ArgT}} <- SuccTypes],
+  ?debug("\n", []),
+  ok.
+-else.
+debug_pp_succ_typings(_) ->
+  ok.
+-endif.
+
+lookup_name(F, CG) ->
+  case dialyzer_callgraph:lookup_name(F, CG) of
+    error -> F;
+    {ok, Name} -> Name
+  end.
+
+send_log(none, _Msg) ->
+  ok;
+send_log(Parent, Msg) ->
+  Parent ! {self(), log, lists:flatten(Msg)},
+  ok.
+
+format_scc(SCC) ->
+  [MFA || {_M, _F, _A} = MFA <- SCC].
+
+%% ============================================================================
+%%
+%%  Debug interface.
+%%
+%% ============================================================================
+
+-spec doit(module() | string()) -> 'ok'.
+
+doit(Module) ->
+  {ok, AbstrCode} = dialyzer_utils:get_abstract_code_from_src(Module),
+  {ok, Code} = dialyzer_utils:get_core_from_abstract_code(AbstrCode),
+  {ok, Records} = dialyzer_utils:get_record_and_type_info(AbstrCode),
+  %% contract typing info in dictionary format
+  {ok, Contracts} =
+    dialyzer_utils:get_spec_info(cerl:concrete(cerl:module_name(Code)),
+                                 AbstrCode, Records),
+  Sigs0 = get_top_level_signatures(Code, Records, Contracts),
+  M = if is_atom(Module) ->  
+	  list_to_atom(filename:basename(atom_to_list(Module)));
+	 is_list(Module) -> 
+	  list_to_atom(filename:basename(Module))
+      end,
+  Sigs1 = [{{M, F, A}, Type} || {{F, A}, Type} <- Sigs0],
+  Sigs = ordsets:from_list(Sigs1),
+  io:format("==================== Final result ====================\n\n", []),
+  pp_signatures(Sigs, Records),
+  ok.
+
+-spec get_top_level_signatures(cerl:c_module(), dict(), dict()) ->
+	 [{{atom(), arity()}, erl_types:erl_type()}].
+
+get_top_level_signatures(Code, Records, Contracts) ->
+  Tree = cerl:from_records(Code),
+  {LabeledTree, NextLabel} = cerl_trees:label(Tree),
+  Plt = get_def_plt(),
+  ModuleName = cerl:atom_val(cerl:module_name(LabeledTree)),
+  Plt1 = dialyzer_plt:delete_module(Plt, ModuleName),
+  Plt2 = analyze_module(LabeledTree, NextLabel, Plt1, Records, Contracts),
+  M = cerl:concrete(cerl:module_name(Tree)),
+  Functions = [{M, cerl:fname_id(V), cerl:fname_arity(V)} 
+	       || {V, _F} <- cerl:module_defs(LabeledTree)],
+  %% First contracts check
+  AllContracts = dict:fetch_keys(Contracts),
+  ErrorContracts = AllContracts -- Functions,  
+  lists:foreach(fun(C) -> 
+		    io:format("Contract for non-existing function: ~w\n",[C])
+		end, ErrorContracts),
+  Types = [{MFA, dialyzer_plt:lookup(Plt2, MFA)} || MFA <- Functions],
+  Sigs = [{{F, A}, erl_types:t_fun(ArgT, RetT)} 
+	  || {{_M, F, A}, {value, {RetT, ArgT}}} <- Types],
+  ordsets:from_list(Sigs).
+
+get_def_plt() ->
+  try 
+    dialyzer_plt:from_file(dialyzer_plt:get_default_plt())
+  catch
+    error:no_such_file -> dialyzer_plt:new();
+    throw:{dialyzer_error, _} -> dialyzer_plt:new()
+  end.
+
+pp_signatures([{{_, module_info, 0}, _}|Left], Records) -> 
+  pp_signatures(Left, Records);
+pp_signatures([{{_, module_info, 1}, _}|Left], Records) -> 
+  pp_signatures(Left, Records);
+pp_signatures([{{M, F, _A}, Type}|Left], Records) ->
+  TypeString =
+    case cerl:is_literal(Type) of
+%% Commented out so that dialyzer does not complain
+%%      false -> 
+%%        "fun(" ++ String = erl_types:t_to_string(Type, Records),
+%%        string:substr(String, 1, length(String)-1);
+      true ->
+	io_lib:format("~w", [cerl:concrete(Type)])
+    end,
+  io:format("~w:~w~s\n", [M, F, TypeString]),
+  pp_signatures(Left, Records);
+pp_signatures([], _Records) ->
+  ok.
+
+-ifdef(DEBUG_PP).
+debug_pp(Tree, _Map) -> 
+  Tree1 = strip_annotations(Tree),
+  io:put_chars(cerl_prettypr:format(Tree1)),
+  io:nl().  
+
+strip_annotations(Tree) ->
+  cerl_trees:map(fun(T) ->
+		     case cerl:is_literal(T) orelse cerl:is_c_values(T) of
+		       true -> cerl:set_ann(T, []);
+		       false ->
+			 Label = cerl_trees:get_label(T),
+			 cerl:set_ann(T, [{'label', Label}])
+		     end
+		 end, Tree).
+-else.
+debug_pp(_Tree, _Map) ->
+  ok.
+-endif. % DEBUG_PP
+
+%%
+%% Analysis of a single module
+%%
+analyze_module(LabeledTree, NextLbl, Plt, Records, Contracts) ->
+  debug_pp(LabeledTree, dict:new()),
+  CallGraph1 = dialyzer_callgraph:new(),
+  CallGraph2 = dialyzer_callgraph:scan_core_tree(LabeledTree, CallGraph1),
+  {CallGraph3, _Ext} = dialyzer_callgraph:remove_external(CallGraph2),
+  CallGraph4 = dialyzer_callgraph:finalize(CallGraph3),
+  CodeServer1 = dialyzer_codeserver:new(),
+  Mod = cerl:concrete(cerl:module_name(LabeledTree)),
+  CodeServer2 = dialyzer_codeserver:insert(Mod, LabeledTree, CodeServer1),
+  CodeServer3 = dialyzer_codeserver:set_next_core_label(NextLbl, CodeServer2),
+  CodeServer4 = dialyzer_codeserver:store_records(Mod, Records, CodeServer3),
+  CodeServer5 = dialyzer_codeserver:store_contracts(Mod, Contracts, CodeServer4),
+  Res = analyze_callgraph(CallGraph4, Plt, CodeServer5),
+  dialyzer_callgraph:delete(CallGraph4),
+  dialyzer_codeserver:delete(CodeServer5),
+  Res.