/*

  $Id$

  Copyright 1989-2016 MINES ParisTech

  This file is part of PIPS.

  PIPS is free software: you can redistribute it and/or modify it
  under the terms of the GNU General Public License as published by
  the Free Software Foundation, either version 3 of the License, or
  any later version.

  PIPS is distributed in the hope that it will be useful, but WITHOUT ANY
  WARRANTY; without even the implied warranty of MERCHANTABILITY or
  FITNESS FOR A PARTICULAR PURPOSE.

  See the GNU General Public License for more details.

  You should have received a copy of the GNU General Public License
  along with PIPS.  If not, see <http://www.gnu.org/licenses/>.

*/
#ifdef HAVE_CONFIG_H
    #include "pips_config.h"
#endif
 /* Interface between the untyped database manager and clean code and
  * between pipsmake and clean code.
  *
  * There are other interface routines in prettyprint.c
  *
  * The top routines should be called by the PIPS make utility. They might
  * eventually be integrated into it.
  *
  * The lower level routines are dealing with "statement_mapping"s. They
  * might have to be updated when mappings are integrated into NewGen.
  * At that time, the whole file should disappear in a typed pipsmake.
  *
  * Francois Irigoin, August 1990
  */

 /* the lowest level routines dealing with "statement_mapping"s are now
  * generated by a macro defined in mapping.h : DEFINE_CURRENT_MAPPING.
  * see this file for more details.
  *
  * Be'atrice Apvrille, August 1993
  */

#include <stdio.h>
#include <string.h>

#include "genC.h"
#include "database.h"

#include "resources.h"
#include "linear.h"
#include "ri.h"
#include "effects.h"
#include "ri-util.h"
#include "workspace-util.h"
#include "effects-util.h"
#include "pipsdbm.h"
#include "effects-generic.h"
#include "effects-simple.h"
#include "control.h"

#include "misc.h"

#include "transformer.h"
/* FC 2015-07-21: redundant declarations to help with include cycle issues
 * there are expected in "transformer.h"
 */
extern transformer (* transformer_fix_point_operator)(transformer);
extern transformer transformer_equality_fix_point(transformer);
extern transformer transformer_pattern_fix_point(transformer);
extern transformer transformer_derivative_fix_point(transformer);

#include "semantics.h"

#include "properties.h"
#include "preprocessor.h"

/* three mappings used throughout semantics analysis:
 *  - transformer_map is computed in a first phase
 *  - precondition_map is computed in a second phase
 *  - cumulated_effects is used and assumed computed before  (defined in effects.c)
 *  - proper_effects might be useless... only DO loop analysis could use it (idem)
 */


/* declaration of the previously described mappings with their access functions :
 *
 * (DEFINE_CURRENT_MAPPING is a macro defined in ~pips/Newgen/mapping.h)
 *
 * BA, August 26, 1993
 */

DEFINE_CURRENT_MAPPING(transformer, transformer)
DEFINE_CURRENT_MAPPING(precondition, transformer)
DEFINE_CURRENT_MAPPING(total_precondition, transformer)

/* Returns the entry to exit transformer associated to a statement,
 * since all statements in PIPS internal representation have a unique
 * exit.
 *
 * The transformers associated to loops are the transformers linking
 * the loop precondition to the loop body precondition. When dealing
 * with sequences or test or... the transformer linking the loop
 * precondition to its postcondition, i.e. the precondition hodling
 * at the loop exit, is needed.
 *
 * To complete the statement transformer, a precondition is
 * required. Different preconditions can be used:
 *
 * - transformer_identity(): provides no information
 *
 * - load_statement_precondition(): provides as much information as
 *   possible
 *
 * - the transformer domain: provides information available when the
 *   transformers are computed, i.e. preconditions do not have to be
 *   available; this is unsafe as the loop entrance transition domain
 *   may be a subset of the precocndition, unless the loop is always
 *   entered.
 *
 * Unlike load_statement_transformer(), this function allocates a new
 * transformer. See comments associated to:
 *
 * generic_complete_statement_transformer()
 */
transformer load_completed_statement_transformer(statement s)
{
  transformer t = load_statement_transformer(s);

  // Unsafe if s is a loop, unless you check that the loop is always
  //entered
  //transformer pre = transformer_to_domain(t);
  transformer pre = transformer_identity();

  transformer te = complete_statement_transformer(t, pre, s);

  //pips_assert("te is defined", !transformer_undefined_p(te));

  free_transformer(pre);

  return te;
}


static void select_fix_point_operator()
{
    if(get_bool_property(SEMANTICS_FIX_POINT)) {
	const char* fp_name = get_string_property("SEMANTICS_FIX_POINT_OPERATOR");
	if(strcmp(fp_name, "transfer")==0) {
	    transformer_fix_point_operator = transformer_equality_fix_point;
	}
	else if(strcmp(fp_name, "pattern")==0) {
	    transformer_fix_point_operator = transformer_pattern_fix_point;
	}
	else if(strcmp(fp_name, "derivative")==0) {
	    transformer_fix_point_operator = transformer_derivative_fix_point;
	}
	else {
	    user_error("select_fix_point_operator", "Unknown value %s for property %s\n",
		       fp_name, "SEMANTICS_FIX_POINT_OPERATOR");
	}
    }
    else {
	transformer_fix_point_operator = transformer_basic_fix_point;
    }
    /* This fix-point is not debugged nor used */
    /*
    if(pips_flag_p(SEMANTICS_INEQUALITY_INVARIANT)) {
      tf = transformer_halbwachs_fix_point(tfb);
    }
    */
}

void add_declaration_list_information(transformer pre,
				      list dl,
				      bool precondition_p)
{
  entity m = get_current_module_entity();
  code c = value_code(entity_initial(m));
  language l = code_language(c);

  FOREACH(ENTITY, v, dl) {
    type t = entity_type(v);

    if(type_variable_p(t)) {
      variable tv = type_variable(t);

      FOREACH(DIMENSION, d, variable_dimensions(tv)) {
	normalized nl = NORMALIZE_EXPRESSION(dimension_lower(d));
	normalized nu = NORMALIZE_EXPRESSION(dimension_upper(d));

	if(normalized_linear_p(nl) && normalized_linear_p(nu)) {
	  Pvecteur vl = normalized_linear(nl);
	  Pvecteur vu = normalized_linear(nu);

	  if(value_mappings_compatible_vector_p(vl) &&
	     value_mappings_compatible_vector_p(vu)) {
	    Pvecteur cv = vect_substract(vl, vu);

	    if(language_c_p(l))
	      vect_add_elem(&cv, TCST, VALUE_MONE);

	    if(!precondition_p) {
	      upwards_vect_rename(cv, pre);
	    }

	    if(!vect_constant_p(cv) || vect_coeff(TCST, cv) > 0) {
	      transformer_inequality_add(pre, cv);
	    }
	  }
	}
      }

    }
  }
}

static void add_declaration_information(transformer pre, entity m, bool precondition_p)
{
  //list decls = code_declarations(value_code(entity_initial(m)));
  list decls = current_module_declarations();

  ifdebug(8) {
      pips_debug(8, "Begin for module %s with precondition\n", module_local_name(m));
      print_transformer(pre);
  }

  add_declaration_list_information(pre, decls, precondition_p);

  ifdebug(8) {
      pips_debug(8, "End for module %s with precondition\n", module_local_name(m));
      print_transformer(pre);
  }

}

static void transformer_add_declaration_information(transformer pre, entity m)
{
  add_declaration_information(pre, m, false);
}

static void precondition_add_declaration_information(transformer pre, entity m)
{
  add_declaration_information(pre, m, true);
}

/* Functions to make transformers */

bool transformers_intra_fast(char * module_name)
{
  bool si = get_bool_property(SEMANTICS_INTERPROCEDURAL);
  bool sfs = get_bool_property(SEMANTICS_FLOW_SENSITIVE);
  bool sfp = get_bool_property(SEMANTICS_FIX_POINT);
  bool result = true;

  /* Set properties as required for a very fast semantics analysis */
  if(si) {
    pips_user_warning("Property SEMANTICS_INTERPROCEDURAL is ignored\n");
    set_bool_property(SEMANTICS_INTERPROCEDURAL, false);
  }
  if(!sfs) {
    pips_user_warning("Property SEMANTICS_FLOW_SENSITIVE is ignored\n");
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
  }
  if(sfp) {
    pips_user_warning("Property SEMANTICS_FIX_POINT is ignored\n");
    set_bool_property(SEMANTICS_FIX_POINT, false);
  }
  /* No need to select a fix point operator given the above property, but just in case... */
  select_fix_point_operator();

  set_bool_property(SEMANTICS_STDOUT, false);
  /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */

  if(get_bool_property("SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT")) {
    pips_user_warning("If you really want to set property "
		      "SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT, "
		      "you should activate TRANSFORMERS_INTER_FULL\n");
  }

  result =  module_name_to_transformers(module_name);

  /* Restaure initial values of modified properties */
  if(si)
    set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
  if(!sfs)
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, false);
  if(sfp)
    set_bool_property(SEMANTICS_FIX_POINT, true);

  return result;
}

bool transformers_intra_full(char * module_name)
{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, false);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, true);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_transformers(module_name);
}

bool transformers_inter_fast(char * module_name)
{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, false);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_transformers(module_name);
}

bool transformers_inter_full(char * module_name)
{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, true);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_transformers(module_name);
}

bool transformers_inter_full_with_points_to(char * module_name)
{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, true);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    set_pt_to_list( (statement_points_to)
		    db_get_memory_resource(DBR_POINTS_TO, module_name, true) );
    bool result = module_name_to_transformers(module_name);
    reset_pt_to_list();

    return result;
}

/* Transformer recomputation cannot be of real use unless an
   interprocedural analysis is performed. For intraprocedural analyses,
   using property SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT is
   sufficient. */
bool refine_transformers_p = false;

bool refine_transformers(char * module_name)
{
  bool res;
  set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
  set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
  set_bool_property(SEMANTICS_FIX_POINT, true);
  select_fix_point_operator();
  set_bool_property(SEMANTICS_STDOUT, false);
  /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
  refine_transformers_p = true;
  res = module_name_to_transformers_in_context(module_name);
  refine_transformers_p = false;
  return res;
}

bool refine_transformers_with_points_to(char * module_name)
{
  bool res;
  set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
  set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
  set_bool_property(SEMANTICS_FIX_POINT, true);
  select_fix_point_operator();
  set_bool_property(SEMANTICS_STDOUT, false);
  /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
  set_pt_to_list( (statement_points_to)
		  db_get_memory_resource(DBR_POINTS_TO, module_name, true) );
  refine_transformers_p = true;
  res = module_name_to_transformers_in_context(module_name);
  refine_transformers_p = false;
  reset_pt_to_list();
  return res;
}

bool summary_transformer(char * module_name)
{
  /* There is a choice: do nothing and leave the effective computation
     in module_name_to_transformers, or move it here */
  /* There is another choice: distinguish between inter- and
     intra-procedural analyses at the summary level or in
     module_name_to_transformers(). The choice does not have to be
     consistent with the similar choice made for summary_precondition. */
  pips_debug(1, "considering module %s\n", module_name);
  return true;
}

bool preconditions_intra(char * module_name)
{
    /* nothing to do: transformers are preconditions for this
       intraprocedural option */

    set_bool_property(SEMANTICS_INTERPROCEDURAL, false);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    /* Maybe we should have an intra fast and an intra full as with other
       semantics entries */
    /* set_bool_property(SEMANTICS_FIX_POINT, false); */
    set_bool_property(SEMANTICS_FIX_POINT, true);
    set_bool_property(SEMANTICS_INEQUALITY_INVARIANT, false);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_preconditions(module_name);
}

bool preconditions_intra_fast(char * module_name)
{
    /* nothing to do: transformers are preconditions for this
       intraprocedural option */

    set_bool_property(SEMANTICS_INTERPROCEDURAL, false);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    /* Maybe we should have an intra fast and an intra full as with other
       semantics entries */
    /* set_bool_property(SEMANTICS_FIX_POINT, false); */
    set_bool_property(SEMANTICS_FIX_POINT, false);
    set_bool_property(SEMANTICS_INEQUALITY_INVARIANT, false);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_preconditions(module_name);
}

bool preconditions_inter_fast(char * module_name)
{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, false);
    set_bool_property(SEMANTICS_INEQUALITY_INVARIANT, false);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_preconditions(module_name);
}

bool preconditions_inter_full(char * module_name)
{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, true);
    set_bool_property(SEMANTICS_INEQUALITY_INVARIANT, false);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_preconditions(module_name);
}

bool preconditions_inter_full_with_points_to(char * module_name)
{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, true);
    set_bool_property(SEMANTICS_INEQUALITY_INVARIANT, false);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    set_pt_to_list( (statement_points_to)
		    db_get_memory_resource(DBR_POINTS_TO, module_name, true) );
    bool result_p = module_name_to_preconditions(module_name);
    reset_pt_to_list();
    return result_p;
}

bool total_preconditions_intra(char * module_name)
{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, false);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, true);
    set_bool_property(SEMANTICS_INEQUALITY_INVARIANT, false);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_total_preconditions(module_name);
}

bool total_preconditions_inter(char * module_name)
{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, true);
    set_bool_property(SEMANTICS_INEQUALITY_INVARIANT, false);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_total_preconditions(module_name);
}


bool old_summary_precondition(char * module_name)
{
  /* do not nothing because it has been computed by side effects;
   * or provide an empty precondition for root modules;
   * maybe a touch to look nicer?
   */

  transformer t;

  debug_on(SEMANTICS_DEBUG_LEVEL);

  debug(8, "summary_precondition", "begin\n");

  if(db_resource_p(DBR_SUMMARY_PRECONDITION, module_name)) {
    /* touch it */
    t = (transformer) db_get_memory_resource(DBR_SUMMARY_PRECONDITION,
					     module_name,
					     true);
  }
  else {
    t = transformer_identity();
  }

  DB_PUT_MEMORY_RESOURCE(DBR_SUMMARY_PRECONDITION,
			 module_name, (char * )t);

  ifdebug(8) {
    pips_debug(8, "initial summary precondition %p for %s:\n",
	       t, module_name);
    dump_transformer(t);
    pips_debug(8, "end\n");
  }

  debug_off();

  return true;
}

bool intraprocedural_summary_precondition(char * module_name)
{
  /* The current module is sufficient to derive it. */
  set_bool_property(SEMANTICS_INTERPROCEDURAL, false);
  return summary_precondition(module_name);
}

bool interprocedural_summary_precondition(char * module_name)
{
  /* The DATA statement from all modules, called or not called, are used,
     as well as the preconditions at all call sites. */
  set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
  return summary_precondition(module_name);
}

static bool use_points_to_information_p = false;

static void set_use_points_to()
{
  use_points_to_information_p = true;
}

static void reset_use_points_to()
{
  use_points_to_information_p = false;
}

bool use_points_to_p()
{
  return use_points_to_information_p;
}


bool interprocedural_summary_precondition_with_points_to(char * module_name)
{
  /* The DATA statement from all modules, called or not called, are
   * used, as well as the preconditions at all call sites. Points_to
   * information is required to perform a more accurate translation
   * between callesr and callees.
   */
  set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
  set_use_points_to();
  bool result_p = summary_precondition(module_name);
  reset_use_points_to();
  return result_p;
}

/* Special case: main module
 *
 * Intraprocedural case: use the local DATA statement to define the initial store.
 *
 * Interprocedural case: use the program precondition
 *
 * */

static transformer main_summary_precondition(entity callee)
{
  transformer t = transformer_undefined;

  if (get_bool_property(SEMANTICS_INTERPROCEDURAL)) {
    t = copy_transformer((transformer)
      db_get_memory_resource(DBR_PROGRAM_PRECONDITION, "", false));
    if(transformer_empty_p(t)) {
      pips_user_warning(
			"Initial preconditions are not consistent.\n"
			" The Fortran standard rules about variable initialization"
			" with DATA statements are likely to be violated.\n"
			"set property PARSER_ACCEPT_ANSI_EXTENSIONS to false\n"
			"and CHECK_FORTRAN_SYNTAX_BEFORE_PIPS to true.\n");
    }
  }
  else {
    /* Do we need to initialize the mappings before calling this subroutine? */
    /* Why not use a DB_GET of DBR_INITIAL_PRECONDITION? */
    /* t = data_to_precondition(callee); */
    t = copy_transformer
      ((transformer) db_get_memory_resource(DBR_INITIAL_PRECONDITION,
					    module_local_name(callee),
					    false));
  }

  return t;
}

/* Standard cases: called modules
 *
 * If a main is present, modules which are never called receive an
 * unfeasible summary_precondition.
 *
 * If no main is present in the current workspace, modules which are never
 * called receive an identity summary precondition, i.e. no information.
 *
 * If an interprocedural analysis is required, the preconditions of all
 * call sites are translated and then unioned.
 *
 *
 */

static transformer ordinary_summary_precondition(const char* module_name,
						 entity callee)
{
  transformer t = transformer_undefined;

  if(get_bool_property(SEMANTICS_INTERPROCEDURAL)) {
    /* Look for all call sites in the callers
     */
    callees callers = (callees) db_get_memory_resource(DBR_CALLERS,
						       module_name,
						       true);
    list lc = callees_callees(callers);

    ifdebug(1) {
      pips_debug(1, "begin for %s with %zd callers\n",
		 module_name,
		 gen_length(lc));
      FOREACH(STRING, caller_name, lc) {
	(void) fprintf(stderr, "%s, ", caller_name);
      }
      (void) fprintf(stderr, "\n");
    }

    reset_call_site_number();
    // FI: it might be safer to make and free this stack in the loop
    // body, once for each caller. The initialization is located in
    // summary_preconditions()

    // make_statement_global_stack();

    FOREACH(STRING, caller_name, callees_callees(callers)) {
      entity caller = module_name_to_entity(caller_name);
      t = update_precondition_with_call_site_preconditions(t, caller, callee);
    }

    // free_statement_global_stack();

    if (ENDP(callees_callees(callers)) &&
	some_main_entity_p()) {
      /* no callers => empty precondition if a main is being analyzed
	 FC. 08/01/1999.
      */
      pips_user_warning("empty precondition to %s "
			"because not in call tree from main.\n", module_name);
      t = transformer_empty();
    }
    else if (transformer_undefined_p(t)) {
      /* No main in the application? Do declare every module executed. */
      t = transformer_identity();
    }
    else {
      /* Try to eliminate (some) redundancy at a reasonnable cost. */
      /* What is a reasonnable cost? */

      t = transformer_normalize(t, 2);
      /* Level 7 core dumps with
       * Semantics-New/summary_precondition04.c unless formal
       * parameter "_c" is renamed... external_value_name is called
       * when the value mapping hash-tables are not
       * available. Validations of Semantics and Semantics-new are not
       * improved by level 7 wrt level 2.
       */
      /* t = transformer_normalize(t, 7); */

      /* Corinne's best one... for YPENT2 in ARC2D, but be ready to pay
	 the price! And in case an overflow occurs, you may loose a lot of
	 accuracy without any control. */
      /* t = transformer_normalize(t, 8); */

      /* No consistency check possible here because value_mappings are
	 not available */
      /* pips_assert("The summary precondition is consistent",
	 transformer_consistency_p(t));*/
    }
  }
  else {
    /* Intraprocedural case */
    t = transformer_identity();
  }

  return t;
}

bool summary_precondition(char * module_name)
{
  /* transformer t = transformer_identity(); */
  transformer t = transformer_undefined;
  entity callee = module_name_to_entity(module_name);

  debug_on(SEMANTICS_DEBUG_LEVEL);

  make_statement_global_stack();
  set_current_module_entity(callee);
  set_current_module_statement((statement) db_get_memory_resource(DBR_CODE, module_name, true));

  if(entity_main_module_p(callee)) {
    t = main_summary_precondition(callee);
  }
  else {
    t = ordinary_summary_precondition(module_name, callee);
  }

  /* Add declaration information: arrays cannot be empty (Fortran
   * standard, Section 5.1.2)
   *
   * It does not seem to be a good idea for the semantics of
   * SUMMARY_PRECONDITION. It seems better to have this information in the
   * summary transformer as an input validity condition.
   *
   */
  if(false && get_bool_property("SEMANTICS_TRUST_ARRAY_DECLARATIONS")) {
    set_cumulated_rw_effects((statement_effects)
			     db_get_memory_resource(DBR_CUMULATED_EFFECTS, module_name, true));
    set_proper_rw_effects((statement_effects)
			     db_get_memory_resource(DBR_PROPER_EFFECTS, module_name, true));
    module_to_value_mappings( get_current_module_entity() );
    transformer_add_declaration_information(t,
					    get_current_module_entity());
    reset_cumulated_rw_effects();
    reset_proper_rw_effects();
    free_value_mappings();
  }

  pips_assert("t is defined", !transformer_undefined_p(t));

  /* Try to put the summary precondition in a (partially) canonical form. */
  t = transformer_normalize(t, 4);
  t = transformer_normalize(t, 4);

  ifdebug(3) {
    pips_debug(1, "considering summary precondition for %s\n", module_name);
    dump_transformer(t);
  }

  DB_PUT_MEMORY_RESOURCE(DBR_SUMMARY_PRECONDITION,
			 module_name, (char * )t);

  ifdebug(1) {
    pips_debug(1,
	       "initial summary precondition %p for %s (%d call sites):\n",
	       t, module_name, get_call_site_number());
    dump_transformer(t);
    pips_debug(1, "end for module %s\n", module_name);
  }

  reset_current_module_statement();
  reset_current_module_entity();
  free_statement_global_stack();
  debug_off();

  return true;
}

bool summary_total_postcondition(char * module_name)
{
  /* Look for all call sites in the callers
   */
  callees callers = (callees) db_get_memory_resource(DBR_CALLERS,
						     module_name,
						     true);
  entity callee = module_name_to_entity(module_name);
  /* transformer t = transformer_identity(); */
  transformer t = transformer_undefined;

  debug_on(SEMANTICS_DEBUG_LEVEL);

  pips_assert("Not implemented yet", false);

  set_current_module_entity(callee);

  ifdebug(1) {
    debug(1, "summary_precondition", "begin for %s with %d callers\n",
	  module_name,
	  gen_length(callees_callees(callers)));
    MAP(STRING, caller_name, {
      (void) fprintf(stderr, "%s, ", caller_name);
    }, callees_callees(callers));
    (void) fprintf(stderr, "\n");
  }

  reset_call_site_number();

  MAP(STRING, caller_name,
  {
    entity caller = module_name_to_entity(caller_name);
    t = update_precondition_with_call_site_preconditions(t, caller, callee);
  }, callees_callees(callers));

  if (!callees_callees(callers) &&
      !entity_main_module_p(callee) &&
      some_main_entity_p())
    {
      /* no callers => empty precondition (but the main).
	 FC. 08/01/1999.
      */
      pips_user_warning("empty precondition to %s "
			"because not in call tree from main.\n", module_name);
      t = transformer_empty();
    } else if (transformer_undefined_p(t)) {
      t = transformer_identity();
    } else {
      /* try to eliminate (some) redundancy at a reasonnable cost */
      /* t = transformer_normalize(t, 2); */

      /* what cost? */
      t = transformer_normalize(t, 7);
    }

  /* Add declaration information: arrays cannot be empty (Fortran
   * standard, Section 5.1.2)
   *
   * It does not seem to be a good idea for the semantics of
   * SUMMARY_PRECONDITION. It seems better to have this information in the
   * summary transformer as an input validity condition.
   *
   */
  if(false && get_bool_property("SEMANTICS_TRUST_ARRAY_DECLARATIONS")) {
    set_current_module_statement(
				 (statement) db_get_memory_resource(DBR_CODE, module_name, true));
    set_cumulated_rw_effects((statement_effects)
			     db_get_memory_resource(DBR_CUMULATED_EFFECTS, module_name, true));
    set_proper_rw_effects((statement_effects)
			     db_get_memory_resource(DBR_PROPER_EFFECTS, module_name, true));
    module_to_value_mappings( get_current_module_entity() );
    transformer_add_declaration_information(t,
					    get_current_module_entity());
    reset_cumulated_rw_effects();
    reset_proper_rw_effects();
    reset_current_module_statement();
    free_value_mappings();
  }

  DB_PUT_MEMORY_RESOURCE(DBR_SUMMARY_TOTAL_POSTCONDITION,
			 module_name, (char * )t);

  ifdebug(1) {
    pips_debug(1,
	       "summary total postcondition %p for %s (%d call sites):\n",
	       t, module_name, get_call_site_number());
    dump_transformer(t);
    pips_debug(1, "end for module %s\n", module_name);
  }

  reset_current_module_entity();
  debug_off();

  return true;
}

bool summary_total_precondition(char * module_name)
{
    /* there is a choice: do nothing and leave the effective computation
       in module_name_to_total_preconditions or move it here */
  pips_debug(1, "considering module %s\n", module_name);
  return true;
}


/* FI: Provisional management of warnings
 *
 * To avoid repetitive warnings.
 *
 * A hash table could be used to count warnings according to the
 * function and line number in the C file.
 */
static int wc = 0;

void set_warning_counters(void)
{
  wc = 0;
}

bool test_warning_counters(void)
{
  return wc++==0;
}


/* bool generic_module_name_to_transformers(char * module_name, bool in_context):
 * compute a transformer for each statement of a module with a given
 * name; compute also the global transformer for the module
 */
bool generic_module_name_to_transformers(const char* module_name, bool in_context)
{
    transformer t_intra = transformer_undefined;
    transformer t_inter = transformer_undefined;
    /* intraprocedural preconditions: proper declarations */
    transformer mod_pre = transformer_undefined;
    list e_inter;

    debug_on(SEMANTICS_DEBUG_LEVEL);
    sc_variable_name_push((char* (*)(Variable)) readable_value_name);

    /* This stack is useful to document warnings and to retrieve
       points-to information. */
    make_statement_global_stack();
    set_warning_counters();
    set_current_module_entity(module_name_to_entity(module_name));
    /* could be a gen_find_tabulated as well... */
    set_current_module_statement(
	(statement) db_get_memory_resource(DBR_CODE, module_name, true));
    if( get_current_module_statement() == (statement) database_undefined )
	pips_internal_error("no statement for module %s", module_name);

    set_proper_rw_effects((statement_effects)
	db_get_memory_resource(DBR_PROPER_EFFECTS, module_name, true));

    set_cumulated_rw_effects((statement_effects)
	db_get_memory_resource(DBR_CUMULATED_EFFECTS, module_name, true));

    set_methods_for_simple_effects();

    /* cumulated_effects_map_print();*/

    e_inter = effects_to_list( (effects)
	db_get_memory_resource(DBR_SUMMARY_EFFECTS, module_name, true));

    set_transformer_map( MAKE_STATEMENT_MAPPING() );

    /* compute the basis related to module m */
    module_to_value_mappings( get_current_module_entity() );

    /* In the main module, transformers can be computed in context of the
       initial values */
    if(entity_main_module_p(get_current_module_entity())
       && get_bool_property("SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT"))
    {
      if (get_bool_property(SEMANTICS_INTERPROCEDURAL))
      {
	mod_pre = (transformer)
	  db_get_memory_resource(DBR_PROGRAM_PRECONDITION, "", false);
	if(transformer_empty_p(mod_pre)) {
	  pips_user_warning(
	     "Initial preconditions are not consistent.\n"
	     " The Fortran standard rules about variable initialization"
	     " with DATA statements are likely to be violated.\n"
	     "set property PARSER_ACCEPT_ANSI_EXTENSIONS to false\n"
	     "and CHECK_FORTRAN_SYNTAX_BEFORE_PIPS to true.\n");
	}
      }
      else
	mod_pre = data_to_precondition(get_current_module_entity());
    }
    else if(in_context) {
      mod_pre =
	transformer_dup(load_summary_precondition(get_current_module_entity()));
    }
    else
      mod_pre = transformer_identity();

    /* Add declaration information: arrays cannot be empty (Fortran
       standard, Section 5.1.2) */
    if(get_bool_property("SEMANTICS_TRUST_ARRAY_DECLARATIONS")) {
      transformer_add_declaration_information(mod_pre,
					      get_current_module_entity());
    }

    /* Get the preconditions: they might prove useful within loops where
       transformers cannot propagate enough information. */
    if(in_context) {
     set_precondition_map( (statement_mapping)
	db_get_memory_resource(DBR_PRECONDITIONS, module_name, true));
   }

    /* compute intraprocedural transformer */
    statement ms = get_current_module_statement();
    t_intra = statement_to_transformer(ms, mod_pre);
    free_transformer(mod_pre);

    DB_PUT_MEMORY_RESOURCE(DBR_TRANSFORMERS, module_name,
			   (char*) get_transformer_map() );

    /* FI: side effect; compute and store the summary transformer, because
       every needed piece of data is available... */

    /* filter out local variables from the global intraprocedural effect */
    t_inter = transformer_intra_to_inter(t_intra, e_inter);
    t_inter = transformer_normalize(t_inter, 2);
    if(c_module_p(get_current_module_entity())) {
      t_inter = value_passing_summary_transformer(get_current_module_entity(), t_inter);
    }
    if(!transformer_consistency_p(t_inter)) {
	(void) print_transformer(t_inter);
	pips_internal_error("Non-consistent summary transformer");
    }
    DB_PUT_MEMORY_RESOURCE(DBR_SUMMARY_TRANSFORMER,
			   module_local_name(get_current_module_entity()),
			   (char*) t_inter);
    pips_debug(8, "t_inter=%p\n", t_inter);

    reset_current_module_entity();
    reset_current_module_statement();
    /* Two auxiliary hash tables allocated by effectsmap_to_listmap() */
    reset_proper_rw_effects();
    reset_cumulated_rw_effects();
    generic_effects_reset_all_methods();
    reset_transformer_map();
    if(in_context) reset_precondition_map();

    free_value_mappings();
    free_statement_global_stack();

    sc_variable_name_pop();
    debug_off();

    return true;
}

bool module_name_to_transformers_in_context(const char* module_name)
{
  bool rc = false;
  bool save_prop = get_bool_property("SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT");

  if(!save_prop) {
    pips_user_warning("Although property SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT"
		      " is not set, it is used because it is necessary for this "
		      "recomputation to be useful\n");
    set_bool_property("SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT", true);
  }

  rc = generic_module_name_to_transformers(module_name, true);

  set_bool_property("SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT", save_prop);
  return rc;
}

bool module_name_to_transformers(const char* module_name)
{
  bool rc = false;
  rc = generic_module_name_to_transformers(module_name, false);
  return rc;
}

/* resource module_name_to_preconditions(char * module_name):
 * compute a transformer for each statement of a module with a given
 * name; compute also the global transformer for the module
 */
bool module_name_to_preconditions(const char* module_name)
{
    transformer t_inter;
    transformer pre;
    transformer post;

    /* set_debug_level(get_int_property(SEMANTICS_DEBUG_LEVEL)); */
    debug_on(SEMANTICS_DEBUG_LEVEL);
    /* To provide information for warnings */
    make_statement_global_stack();
    sc_variable_name_push((char* (*)(Variable)) readable_value_name);

    set_current_module_entity(module_name_to_entity(module_name) );
    /* could be a gen_find_tabulated as well... */
    set_current_module_statement(
	(statement) db_get_memory_resource(DBR_CODE, module_name, true));
    if(get_current_module_statement() == (statement) database_undefined)
	pips_internal_error("no statement for module %s", module_name);

    /* Used to add reference information when it is trusted... which
       should always be, at least for automatic parallelization. */
    set_proper_rw_effects((statement_effects)
	db_get_memory_resource(DBR_PROPER_EFFECTS, module_name, true));

    /* cumulated effects are used to compute the value mappings */
    set_cumulated_rw_effects((statement_effects)
	db_get_memory_resource(DBR_CUMULATED_EFFECTS, module_name, true));

    set_methods_for_simple_effects();

    set_transformer_map( (statement_mapping)
	db_get_memory_resource(DBR_TRANSFORMERS, module_name, true));


    /* p_inter is not used!!! FI, 9 February 1994 */
    /*
    if(get_bool_property(SEMANTICS_INTERPROCEDURAL)) {
	p_inter = (transformer)
	    db_get_memory_resource(DBR_SUMMARY_PRECONDITION,
				   module_name, true);
    }
    */

    t_inter = (transformer)
	db_get_memory_resource(DBR_SUMMARY_TRANSFORMER, module_name, true);

    /* debug_on(SEMANTICS_DEBUG_LEVEL); */

    set_precondition_map( MAKE_STATEMENT_MAPPING() );

    /* compute the mappings related to module m, that is likely to be
       unavailable during interprocedural analysis; a module reference
       should be kept with the mappings to avoid useless recomputation,
       allocation and frees, including those due to the prettyprinter */

    module_to_value_mappings( get_current_module_entity() );

    /* set the list of global values. This is a bit too restrictive in
       C as the formal arguments, even modified in the procedure body,
       will not appear in the transformer_arguments. Should we add
       missing formal arguments to this list? See for instance
       "character01.c". */
    set_module_global_arguments(transformer_arguments(t_inter));

    /* debug_on(SEMANTICS_DEBUG_LEVEL); */

    pre = copy_transformer(load_summary_precondition(get_current_module_entity()));

    /* Add declaration information: arrays cannot be empty (Fortran
       standard, Section 5.1.2). But according to summary_precondition(),
       this is now supposed to be performed by the transformer phase? */
    if(get_bool_property("SEMANTICS_TRUST_ARRAY_DECLARATIONS")) {
        precondition_add_declaration_information(pre, get_current_module_entity());
    }
    if(get_bool_property("SEMANTICS_USE_TYPE_INFORMATION")
       || get_bool_property("SEMANTICS_USE_TYPE_INFORMATION_IN_PRECONDITIONS")) {

      /* If the module is never called, its precondition is identity
	 and by default no values are listed in its basis. Function
	 add_type_information() has no effect. */

      /* if(transformer_identity_p(pre)) { */
      /* 	list el = effects_to_list( */
      /* 			       (effects) db_get_memory_resource(DBR_SUMMARY_EFFECTS, module_name, true)); */
      /* 	free_transformer(pre); */
      /* 	// FI: memory leak  */
      /* 	pre = transformer_range(effects_to_transformer(el)); */
      /* } */

      transformer_add_type_information(pre);
    }

    /* debug_on(SEMANTICS_DEBUG_LEVEL); */

    /* propagate the module precondition */
    init_reachable(get_current_module_statement());
    post = statement_to_postcondition(pre, get_current_module_statement() );
    close_reachable();

    /* post could be stored in the ri for later interprocedural uses
       but the ri cannot be modified so early before the DRET demo;
       also our current interprocedural algorithm does not propagate
       postconditions upwards in the call tree */

    DB_PUT_MEMORY_RESOURCE(DBR_PRECONDITIONS,
			   module_name,
			   (char*) get_precondition_map() );

    pips_debug(8, "postcondition computed for %s\n",
	  entity_local_name( get_current_module_entity() ));
    ifdebug(8) (void) print_transformer(post);
    debug(1, "module_name_to_preconditions", "end\n");

    reset_current_module_entity();
    reset_current_module_statement();
    reset_transformer_map();
    reset_precondition_map();
    reset_proper_rw_effects();
    reset_cumulated_rw_effects();
    generic_effects_reset_all_methods();

    free_value_mappings();

    sc_variable_name_pop();
    free_statement_global_stack();
    debug_off();

    return true;
}

bool module_name_to_total_preconditions(const char* module_name)
{
  transformer t_inter = transformer_undefined;
  transformer t_pre = transformer_undefined;
  transformer t_pre_inter = transformer_undefined;
  transformer t_post = transformer_undefined;
  list e_inter = list_undefined;

  debug_on(SEMANTICS_DEBUG_LEVEL);
  sc_variable_name_push((char* (*)(Variable)) readable_value_name);

  set_current_module_entity(module_name_to_entity(module_name) );
  set_current_module_statement(
			       (statement) db_get_memory_resource(DBR_CODE, module_name, true));
  if(get_current_module_statement() == (statement) database_undefined)
    pips_internal_error("no statement for module %s", module_name);

  set_proper_rw_effects((statement_effects)
			db_get_memory_resource(DBR_PROPER_EFFECTS, module_name, true));

  set_cumulated_rw_effects((statement_effects)
			   db_get_memory_resource(DBR_CUMULATED_EFFECTS, module_name, true));

  e_inter = effects_to_list((effects)
			    db_get_memory_resource(DBR_SUMMARY_EFFECTS, module_name, true));

  set_transformer_map( (statement_mapping)
		       db_get_memory_resource(DBR_TRANSFORMERS, module_name, true));

  set_precondition_map( (statement_mapping)
		       db_get_memory_resource(DBR_PRECONDITIONS, module_name, true));


  t_inter = (transformer)
    db_get_memory_resource(DBR_SUMMARY_TRANSFORMER, module_name, true);

  set_total_precondition_map( MAKE_STATEMENT_MAPPING() );

  module_to_value_mappings( get_current_module_entity() );

  /* set the list of global values */
  set_module_global_arguments(transformer_arguments(t_inter));

  if(entity_main_module_p(get_current_module_entity())) {
    /* The program postcondition should be used DBR_PROGRAM_POSTCONDITION */
    t_post = transformer_identity();
  }

  ifdebug(3) {
    pips_debug(1, "considering final total postcondition for %s\n", module_name);
    print_transformer(t_post);
  }

  if(get_bool_property(SEMANTICS_INTERPROCEDURAL)) {
    transformer ip =
      load_summary_total_postcondition(get_current_module_entity());
    if( ip == transformer_undefined) {
      /* that might be because we are at the call tree root
	 or because no information is available;
	 maybe, every module precondition should be initialized
	 to a neutral value? */
      pips_user_warning("no interprocedural module total postcondition for %s\n",
			entity_local_name(get_current_module_entity() ));
      ;
    }
    else {
      translate_global_values(get_current_module_entity(), ip);
      ifdebug(8) {
	pips_debug(8, "\t summary_total_postcondition %p after translation:\n",
		   ip);
	print_transformer(ip);
	pips_assert("The summary total postcondition is consistent",
		    transformer_consistency_p(ip));
      }
      t_post = transformer_combine(transformer_dup(ip), t_post);
    }
  }
  else if(transformer_undefined_p(t_post)) {
    /* intra-procedural case, not a main module */
    t_post = transformer_identity();
  }

  /* propagate the module total postcondition */
  init_reachable(get_current_module_statement());
  t_pre = statement_to_total_precondition(t_post, get_current_module_statement() );
  close_reachable();

  DB_PUT_MEMORY_RESOURCE(DBR_TOTAL_PRECONDITIONS,
			 module_name,
			 (char*) get_total_precondition_map() );

  /* filter out local variables from the global intraprocedural effect */
  t_pre_inter = transformer_intra_to_inter(t_pre, e_inter);
  t_pre_inter = transformer_normalize(t_pre_inter, 2);
  if(!transformer_consistency_p(t_pre_inter)) {
    (void) print_transformer(t_pre_inter);
    pips_internal_error("Non-consistent summary transformer");
  }
  DB_PUT_MEMORY_RESOURCE(DBR_SUMMARY_TOTAL_PRECONDITION,
			 module_local_name(get_current_module_entity()),
			 (char*) t_pre_inter);

  pips_debug(8, "total precondition computed for %s\n",
	     entity_local_name( get_current_module_entity() ));
  ifdebug(8) (void) print_transformer(t_pre);
  pips_debug(1, "end\n");

  reset_current_module_entity();
  reset_current_module_statement();
  reset_transformer_map();
  reset_precondition_map();
  reset_total_precondition_map();
  reset_proper_rw_effects();
  reset_cumulated_rw_effects();

  free_value_mappings();

  sc_variable_name_pop();
  debug_off();

  return true;
}


transformer load_summary_transformer(entity e)
{
    /* FI: I had to add a guard db_resource_p() on Nov. 14, 1995.
     * I do not understand why the problem never occured before,
     * although it should each time the intra-procedural option
     * is selected.
     *
     * This may partially be explained because summary transformers
     * are implicitly computed with transformers instead of using
     * an explicit call to summary_transformer (I guess I'm going
     * to change that).
     *
     * I think it would be better not to call load_summary_transformer()
     * at all when no interprocedural options are selected. I should
     * change that too.
     */

    /* memoization could be used to improve efficiency */
    transformer t = transformer_undefined;

    pips_assert("e is a module", entity_module_p(e));

    if(db_resource_p(DBR_SUMMARY_TRANSFORMER, module_local_name(e))) {
	t = (transformer)
	    db_get_memory_resource(DBR_SUMMARY_TRANSFORMER,
				   entity_local_name(e),
				   true);

	/* db_get_memory_resource never returns database_undefined or
	   resource_undefined */
	pips_assert("load_summary_transformer", t != transformer_undefined);
    }
    else {
	t = transformer_undefined;
    }

    /* Let's be careful with people using an intraprocedural analysis
       of the transformers and requesting an interprocedural analysis
       of the preconditions... */
    if(transformer_undefined_p(t)) {
      if(db_resource_p(DBR_SUMMARY_EFFECTS, module_local_name(e))) {
	list el = effects_effects((effects)
				  db_get_memory_resource(DBR_SUMMARY_EFFECTS,
							 entity_local_name(e),
							 true));
	t = effects_to_transformer(el);
      }
    }

    return t;
}


/* void update_summary_precondition(e, t): t is supposed to be a
 * precondition related to one of e's call sites and translated into
 * e's basis;
 *
 * the current global precondition for e is replaced by its convex
 * hull with t;
 *
 * t may be slightly modified by transformer_convex_hull
 * because of bad design (FI)
 */
void update_summary_precondition(entity e, transformer t)
{
    transformer t_old = transformer_undefined;
    transformer t_new = transformer_undefined;

    pips_assert("update_summary_precondition", entity_module_p(e));

    debug(8, "update_summary_precondition", "begin\n");

    t_old = (transformer)
	db_get_memory_resource(DBR_SUMMARY_PRECONDITION, module_local_name(e),
			       true);

    ifdebug(8) {
	debug(8, "update_summary_precondition", " old precondition for %s:\n",
	      entity_local_name(e));
	print_transformer(t_old);
    }

    if(t_old == transformer_undefined)
	t_new = transformer_dup(t);
    else {
	t_new = transformer_convex_hull(t_old, t);
	transformer_free(t_old);
    }

    DB_PUT_MEMORY_RESOURCE(DBR_SUMMARY_PRECONDITION,
			   module_local_name(e),
			   (char*) t_new );

    ifdebug(8) {
	debug(8, "update_summary_precondition", "new precondition for %s:\n",
	      entity_local_name(e));
	print_transformer(t_new);
	debug(8, "update_summary_precondition", "end\n");
    }
}

/* summary_preconditions are expressed in any possible frame, in fact the frame of
 * the last procedure that used/produced it
 */
transformer load_summary_precondition(entity e)
{
  /* memoization could be used to improve efficiency */
  transformer t;

  pips_assert("e is a module", entity_module_p(e));

  pips_debug(8, "begin\n for %s\n",
	     module_local_name(e));

  t = (transformer)
    db_get_memory_resource(DBR_SUMMARY_PRECONDITION, module_local_name(e),
			   true);
  /* Not done earlier, because the value mappings were not available. On
     the other hand, htis assumes that the value mappings have been
     initialized before a call to load_summary_precondition(0 is
     performed.*/
  translate_global_values(e, t);

  pips_assert("the summary precondition t is defined", t != transformer_undefined);

  ifdebug(8) {
    pips_debug(8, " precondition for %s:\n",
	       module_local_name(e));
    dump_transformer(t);
    pips_debug(8, " end\n");
  }

  return t;
}

/* summary_preconditions are expressed in any possible frame, in fact the frame of
 * the last procedure that used/produced it
 */
transformer load_summary_total_postcondition(entity e)
{
    transformer t_post = transformer_undefined;;

    pips_assert("e is a module", entity_module_p(e));

    pips_debug(8, "begin\n for %s\n",
	  module_local_name(e));

    t_post = (transformer)
	db_get_memory_resource(DBR_SUMMARY_TOTAL_POSTCONDITION, module_local_name(e),
			       true);

    pips_assert("t is defined", t_post != transformer_undefined);

    ifdebug(8) {
	pips_debug(8, " total postcondition for %s:\n",
	      module_local_name(e));
	dump_transformer(t_post);
	pips_debug(8, " end\n");
    }

    return t_post;
}

/* FI->FI, FI->BC: these two functions should be moved into
   effects-util or effects-simple */
list load_summary_effects(entity e)
{
    /* memorization could be used to improve efficiency */
    list t;

    pips_assert("load_summary_effects", entity_module_p(e));

    t = effects_to_list( (effects)
	db_get_memory_resource(DBR_SUMMARY_EFFECTS, module_local_name(e),
			       true));

    pips_assert("t is defined", t != list_undefined);

    return t;
}

list load_body_effects(entity e)
{
  string module_name = (string) module_local_name(e);

    pips_assert("load_summary_effects", entity_module_p(e));

    statement b = (statement) db_get_memory_resource(DBR_CODE, module_name, true);
    statement_effects se = (statement_effects)
      db_get_memory_resource(DBR_CUMULATED_EFFECTS, module_name, true);
    effects be = (effects) (intptr_t)HASH_GET(p, p, statement_effects_hash_table(se), (void *) b);
    list bel = effects_effects(be);

    pips_assert("bel is defined", bel != list_undefined);

    return bel;
}


list load_module_intraprocedural_effects(entity e)
{
    /* memoization could be used to improve efficiency */
    list t;
    statement s;

    pips_assert("is a module", entity_module_p(e));
    pips_assert("is the current module", e == get_current_module_entity());
    s = get_current_module_statement();
    pips_assert("some statement", s!=statement_undefined);

    t = load_cumulated_rw_effects_list(s);

    pips_assert("some list", t != list_undefined);

    return t;
}


/* ca n'a rien a` faire ici, et en plus, il serait plus inte'ressant
 * d'avoir une fonction void statement_map_print(statement_mapping
 * htp)
 */
void cumulated_effects_map_print(void)
{
    FILE * f =stderr;
    statement_effects htp = get_cumulated_rw_effects();

    /* hash_table_print_header (htp,f); */

    STATEMENT_EFFECTS_MAP(k, v, {
	fprintf(f, "\n\n%td", statement_ordering((statement) k));
	print_effects( effects_effects(v));
    },
      htp);
}