PIPS
|
#include <stdio.h>
#include <string.h>
#include "boolean.h"
#include "vecteur.h"
#include "contrainte.h"
#include "sc.h"
#include "genC.h"
#include "linear.h"
#include "ri.h"
#include "effects.h"
#include "ri-util.h"
#include "prettyprint.h"
#include "effects-util.h"
#include "misc.h"
#include "semantics.h"
#include "transformer.h"
Go to the source code of this file.
Macros | |
#define | StorePost(stat, val) |
#define | StorePre(stat, val) |
#define | LoadPost(stat) |
#define | LoadPre(stat) |
Functions | |
static bool | postcondition_filter (statement stat) |
filter used by gen_recurse: Top-down computation of the postcondition mapping More... | |
statement_mapping | compute_postcondition (statement stat, statement_mapping post_map, statement_mapping pre_map) |
statement_mapping compute_postcondition(stat, post_map, pre_map) statement stat; statement_mapping post_map, pre_map; More... | |
Variables | |
static statement_mapping | current_precondition_map = hash_table_undefined |
filtering of postconditions More... | |
static statement_mapping | current_postcondition_map = hash_table_undefined |
#define LoadPost | ( | stat | ) |
Definition at line 77 of file postcondition.c.
#define LoadPre | ( | stat | ) |
Definition at line 81 of file postcondition.c.
#define StorePost | ( | stat, | |
val | |||
) |
Definition at line 69 of file postcondition.c.
#define StorePre | ( | stat, | |
val | |||
) |
Definition at line 73 of file postcondition.c.
statement_mapping compute_postcondition | ( | statement | stat, |
statement_mapping | post_map, | ||
statement_mapping | pre_map | ||
) |
statement_mapping compute_postcondition(stat, post_map, pre_map) statement stat; statement_mapping post_map, pre_map;
computes the postcondition mapping post_map from the precondition mapping pre_map and the related statement tree starting from stat. The rule applied is that the postcondition of one statement is the precondition of the following one. The last postcondition is arbitrary set to transformer_identity, what is not enough. (??? should I take the stat transformer?)
the initial postcondition is empty ???
Top-down definition
stat | tat |
post_map | ost_map |
pre_map | re_map |
Definition at line 186 of file postcondition.c.
References current_postcondition_map, current_precondition_map, debug_off, debug_on, gen_null(), gen_recurse, hash_table_undefined, pips_debug, postcondition_filter(), statement_domain, StorePost, and transformer_identity().
Referenced by set_resources_for_module().
filter used by gen_recurse: Top-down computation of the postcondition mapping
??? may happen in obscure unstructured...
??? may be false...
??? is just false...
generates the full list
???
must go downward
Definition at line 88 of file postcondition.c.
References blocks, CONTROL, CONTROL_MAP, control_statement, gen_copy_seq(), gen_free_list(), gen_nreverse(), ifdebug, instruction_block, instruction_loop, instruction_tag, instruction_test, instruction_unstructured, is_instruction_block, is_instruction_call, is_instruction_goto, is_instruction_loop, is_instruction_test, is_instruction_unstructured, LoadPost, LoadPre, loop_body, MAP, NIL, pips_debug, pips_internal_error, print_statement(), STATEMENT, statement_instruction, StorePost, test_false, test_true, transformer_undefined_p, and unstructured_control.
Referenced by compute_postcondition().
|
static |
Definition at line 67 of file postcondition.c.
Referenced by compute_postcondition().
|
static |
filtering of postconditions
Standard includes Psystems stuff Newgen stuff PIPS stuff
Definition at line 66 of file postcondition.c.
Referenced by compute_postcondition().