25 #include "pips_config.h"
58 #include "resources.h"
95 pips_assert(
"consistent initial precondition before filtering",
129 #define pred_debug(level, msg, trans) \
130 ifdebug(level) { pips_debug(level, msg); dump_transformer(trans);}
151 pips_debug(1,
"considering program \"%s\" with main \"%s\"\n", name,
183 pips_assert(
"some modules in the program", nmodules>0);
185 for(i=0; i<nmodules; i++) {
188 pips_debug(1,
"considering module %s\n", mname);
197 pred_debug(3,
"to be added after translation:\n", tm);
204 pred_debug(3,
"to be added after filtering:\n", tm);
210 pred_debug(1,
"resulting program precondition:\n", t);
243 pips_debug(1,
"considering program \"%s\" with main \"%s\"\n", name,
246 pred_debug(1,
"assumed program postcondition:\n", post);
void free_transformer(transformer p)
size_t gen_array_nitems(const gen_array_t a)
void gen_array_full_free(gen_array_t a)
void * gen_array_item(const gen_array_t a, size_t i)
transformer transformer_dup(transformer t_in)
transformer package - basic routines
transformer transformer_identity()
Allocate an identity transformer.
bool transformer_consistency_p(transformer t)
FI: I do not know if this procedure should always return or fail when an inconsistency is found.
void reset_proper_rw_effects(void)
void set_proper_rw_effects(statement_effects)
void set_cumulated_rw_effects(statement_effects)
void reset_cumulated_rw_effects(void)
list effects_to_list(effects)
void reset_current_module_entity(void)
Reset the current module entity.
void reset_current_module_statement(void)
Reset the current module statement.
statement set_current_module_statement(statement)
Set the current module statement.
entity set_current_module_entity(entity)
static.c
#define NIL
The empty list (nil in Lisp)
string db_get_memory_resource(const char *rname, const char *oname, bool pure)
Return the pointer to the resource, whatever it is.
gen_array_t db_get_module_list(void)
Get an array of all the modules (functions, procedures and compilation units) of a workspace.
#define DB_PUT_MEMORY_RESOURCE(res_name, own_name, res_val)
conform to old interface.
bool program_precondition(const string name)
Compute the union of all initial preconditions.
bool initial_precondition(string name)
Compute an initial transformer.
#define pred_debug(level, msg, trans)
bool program_postcondition(const string name)
The program correctness postcondition cannot be infered.
static void intersect(transformer t1, transformer t2)
returns t1 inter= t2;
bool print_initial_precondition(const string name)
bool print_program_precondition(const string name)
#define pips_debug
these macros use the GNU extensions that allow variadic macros, including with an empty list.
#define pips_assert(what, predicate)
common macros, two flavors depending on NDEBUG
#define pips_internal_error
string get_main_entity_name(void)
Return the local name of the main module if it is available, or the local name of any module by defau...
#define print_transformer(t)
bool make_text_resource_and_free(const char *, const char *, const char *, text)
entity module_name_to_entity(const char *mn)
This is an alias for local_name_to_top_level_entity.
const char * module_local_name(entity e)
Returns the module local user name.
void free_statement_global_stack(void)
void make_statement_global_stack(void)
#define transformer_relation(x)
struct _newgen_struct_transformer_ * transformer
#define predicate_system(x)
transformer all_data_to_precondition(entity m)
any variable is included.
Psysteme sc_append(Psysteme s1, Psysteme s2)
Psysteme sc_append(Psysteme s1, Psysteme s2): calcul de l'intersection des polyedres definis par s1 e...
void translate_global_values(entity m, transformer tf)
void module_to_value_mappings(entity m)
void module_to_value_mappings(entity m): build hash tables between variables and values (old,...
text text_transformer(transformer tran)
text text_transformer(transformer tran) input : a transformer representing a transformer or a precond...
The structure used to build lists in NewGen.