PIPS
|
#include <stdio.h>
#include <string.h>
#include "genC.h"
#include "linear.h"
#include "ri.h"
#include "effects.h"
#include "ri-util.h"
#include "effects-util.h"
#include "database.h"
#include "pipsdbm.h"
#include "resources.h"
#include "misc.h"
#include "effects-generic.h"
#include "effects-simple.h"
#include "prettyprint.h"
#include "transformer.h"
#include "semantics.h"
Go to the source code of this file.
Macros | |
#define | pred_debug(level, msg, trans) ifdebug(level) { pips_debug(level, msg); dump_transformer(trans);} |
Functions | |
bool | initial_precondition (string name) |
Compute an initial transformer. More... | |
static void | intersect (transformer t1, transformer t2) |
returns t1 inter= t2; More... | |
bool | program_precondition (const string name) |
Compute the union of all initial preconditions. More... | |
bool | program_postcondition (const string name) |
The program correctness postcondition cannot be infered. More... | |
bool | print_initial_precondition (const string name) |
bool | print_program_precondition (const string name) |
#define pred_debug | ( | level, | |
msg, | |||
trans | |||
) | ifdebug(level) { pips_debug(level, msg); dump_transformer(trans);} |
Compute an initial transformer.
Filter out local and unused variables from the local precondition? No, because it is not possible to guess what is used or unused at the program level. Filtering is postponed to program_precondition().
name | ame |
Definition at line 75 of file initial.c.
References all_data_to_precondition(), db_get_memory_resource(), DB_PUT_MEMORY_RESOURCE, debug_off, debug_on, free_statement_global_stack(), free_value_mappings(), ifdebug, make_statement_global_stack(), module, module_name_to_entity(), module_to_value_mappings(), pips_assert, reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), reset_proper_rw_effects(), set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), set_proper_rw_effects(), strdup(), and transformer_consistency_p().
|
static |
returns t1 inter= t2;
Definition at line 120 of file initial.c.
References predicate_system, sc_append(), and transformer_relation.
Referenced by program_precondition().
name | ame |
Definition at line 261 of file initial.c.
References db_get_memory_resource(), debug_off, debug_on, free_value_mappings(), make_text_resource_and_free(), module, module_name_to_entity(), module_to_value_mappings(), ok, reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), and text_transformer().
A small function that would require pipsdbm and ri-util
name | ame |
Definition at line 293 of file initial.c.
References db_get_memory_resource(), debug_off, debug_on, free(), free_value_mappings(), get_main_entity_name(), make_text_resource_and_free(), module_local_name(), module_name_to_entity(), module_to_value_mappings(), ok, pips_debug, reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), and text_transformer().
The program correctness postcondition cannot be infered.
It should be provided by the user.
A small function that would require pipsdbm and ri-util
name | ame |
Definition at line 233 of file initial.c.
References DB_PUT_MEMORY_RESOURCE, debug_off, debug_on, free(), get_main_entity_name(), ifdebug, module_local_name(), module_name_to_entity(), pips_assert, pips_debug, pred_debug, transformer_consistency_p(), and transformer_identity().
Compute the union of all initial preconditions.
A small function that would require pipsdbm and ri-util
e_inter = effects_to_list(get_cumulated_rw_effects(get_current_module_statement()));
Unavoidable pitfall: initializations in uncalled modules may be taken into account. It all depends on the "create" command.
no dup & false => core
modifies tm!
tm = transformer_normalize(tm, 2);
name | ame |
Definition at line 134 of file initial.c.
References db_get_memory_resource(), db_get_module_list(), DB_PUT_MEMORY_RESOURCE, debug_off, debug_on, effects_to_list(), entity_undefined, free(), free_statement_global_stack(), free_transformer(), free_value_mappings(), gen_array_full_free(), gen_array_item(), gen_array_nitems(), get_main_entity_name(), ifdebug, intersect(), make_statement_global_stack(), module_local_name(), module_name_to_entity(), module_to_value_mappings(), NIL, pips_assert, pips_debug, pips_internal_error, pred_debug, print_transformer, reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), reset_proper_rw_effects(), set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), set_proper_rw_effects(), transformer_consistency_p(), transformer_dup(), transformer_identity(), transformer_intra_to_inter(), and translate_global_values().