25 #include "pips_config.h"
98 #include "constants.h"
125 "ctr %p, %zd preds, %zd succs: %s",
130 fprintf(stderr,
"\tsuccessors:\n");
132 fprintf(stderr,
"\t\t%p %s", s,
135 fprintf(stderr,
"\tpredecessors:\n");
137 fprintf(stderr,
"\t\t%p %s", p,
146 fprintf(stderr,
"empty control list");
195 pips_debug(2,
"Begin for node %p and statement %s\n", c,
224 pips_assert(
"The predecessor's postcondition npre is defined",
237 pips_debug(2,
"End for node %p and statement %s with precondition %p:\n", c,
252 pips_debug(6,
"Store postcondition for control %p: %s\n",
258 pips_assert(
"The postcondition to insert is consistent",
261 pips_assert(
"The postcondition is not defined yet",
265 (
void *) c, (
void *) post);
275 pips_assert(
"The postcondition is already defined",
282 pips_debug(6,
"Update postcondition for control %p and statement %s:\n",
291 (
void *)c, (
void *) post);
300 fprintf(stderr,
"Control %p, Statement %s, Temporary postcondition:\n",
303 }, control_postcondition_map);
306 pips_assert(
"The CFG contains at least one node with one statement",
315 return control_postcondition_map;
323 }, control_postcondition_map);
371 pips_debug(5,
"control %p, ancestor %p, transformer %p\n", c, c_a, fptf);
389 pips_debug(8,
"Store fix_point for control %p: %s\n",
395 pips_assert(
"The fix_point to insert is consistent",
402 (
void *)c, (
void *) fptf);
409 return control_fix_point_map;
417 }, control_fix_point_map);
428 list to_be_processed,
429 list still_to_be_processed,
430 list already_processed,
450 pips_assert(
"Postcondition for unreachable nodes must be empty",
481 pips_debug(2,
"Failed for predecessor node pred=%p and node c=%p with map %p:\n",
482 pred, c, control_postcondition_map);
483 pips_assert(
"postconditions of predecessors are assumed initialized"
484 " (see process_ready_node().",
false);
493 pips_assert(
"c does not appear more than twice in the successor list",
525 string msg =
control_test_p(pred)? (i%2==1?
"true" :
"false"):
"standard";
526 pips_debug(2,
"End for %s arc of position %d between predecessor node pred=%p"
527 " and node c=%p with precondition %p:\n",
528 msg, i, pred, c, pre);
564 pips_debug(6,
"Effect list for unstructured %p with entry %p:begin\n",
580 pips_debug(7,
"Sub-effect list for unstructured %p with entry %p:\n",
583 pips_debug(7,
"Union with previous effects:\n");
598 pips_debug(6,
"Effect list for unstructured %p with entry %p:end\n",
611 pips_debug(6,
"Effect list for unstructured %p with entry %p:\n",
639 bool postcondition_p)
647 pips_debug(2,
"Begin for control %p with pre_entry=%p:\n", c, pre_entry);
649 pips_debug(2,
"Begin with n_pre=%p:\n", n_pre);
684 pips_debug(2,
"Precondition %p for control %p:\n", pre, c);
697 pips_debug(2,
"Refined precondition %p for control %p:\n", pre, c);
722 pips_debug(6,
"Rough fixpoint transformer %p for unstructured %p:\n", tf_u, scc_u);
724 pips_debug(6,
"Resulting in generic node precondition %p:\n", n_pre_u);
739 control_postcondition_map,
743 pips_debug(2,
"Fixpoint transformer %p for control %p:\n", fptf, c);
774 pips_debug(2,
"Precondition after cycle execution %p for control %p:\n", pre, c);
776 pips_debug(2,
"derived from pre_cycle %p:\n", pre_cycle);
778 pips_debug(2,
"and from pre_no_cycle %p:\n", pre_no_cycle);
789 if(postcondition_p) {
804 pips_assert(
"The statement transformer is defined",
809 pips_debug(2,
"Postcondition %p for control %p:\n", post, c);
857 pips_debug(2,
"Postcondition %p stored for control %p:\n", post, c);
864 bool postcondition_p)
880 if(postcondition_p) {
900 else if(postcondition_p
912 " postcondtion for unexpected unreachable node:%s",
915 else if(!postcondition_p
921 " transformer for unexpected unreachable node:%s",
942 (
void *) d, (
void *) dependencies);
957 (
void *) d, (
void *) dependencies);
958 }, cycle_dependencies_map);
982 pips_debug(2,
"No previous precondition. Current one %p:\n", pre);
988 hash_update(precondition_map, k, (
void *) n_t_pre);
989 pips_debug(2,
"Previous precondition %p:\n", t_pre);
991 pips_debug(2,
"New precondition %p:\n", n_t_pre);
1003 ((
void *) s, pre, (
hash_table) statement_temporary_precondition_map);
1011 fprintf(stderr,
"Statement %s, Temporary precondition:\n",
1014 }, statement_temporary_precondition_map);
1017 pips_assert(
"The DAG contains at least one control node with one statement",
false);
1029 ((
void *) c, pre, (
hash_table) cycle_temporary_precondition_map);
1032 pips_debug(6,
"Precondition %p for cycle %p:\n", pre, c);
1058 pips_assert(
"The cycle precondition is available",
1062 pips_debug(6,
"Precondition %p for cycle %p:\n", t_pre, c_a);
1074 pips_assert(
"The cycle precondition is available",
1095 list still_to_be_processed =
NIL;
1103 pips_assert(
"Please the compiler", partition==partition);
1105 cycle_temporary_precondition_map==cycle_temporary_precondition_map);
1122 while(!
ENDP(still_to_be_processed)) {
1128 pips_debug(5,
"Try forward processing for\n");
1132 for(l=still_to_be_processed; !
ENDP(l); ) {
1137 still_to_be_processed,
1139 control_postcondition_map)) {
1183 (c_a, e_pre, cycle_temporary_precondition_map);
1195 (c_s, e_pre, statement_temporary_precondition_map);
1205 statement_temporary_precondition_map);
1208 ancestor_map, scc_map);
1225 if(!
ENDP(still_to_be_processed)) {
1226 pips_assert(
"still_to_be_processed is empty because of the Bourdoncle's restructuring",
1248 list still_to_be_processed =
NIL;
1255 pips_debug(2,
"Begin with control_postcondition_map=%p:\n",
1256 control_postcondition_map);
1267 for(c_c = nl; !
ENDP(c_c);
POP(c_c)) {
1334 pips_debug(2,
"\nPreconditions for statements after ND DAG processing:\n");
1336 pips_debug(2,
"End of preconditions for statements after ND DAG processing:\n\n");
1369 pips_debug(2,
"Compute dependencies for %d cycle%s\n",
1380 pips_debug(8,
"Compute dependencies for cycle %p with statement %s\n",
1385 for(c_cc=nl; !
ENDP(c_cc);
POP(c_cc)) {
1413 still_to_be_processed =
CONS(
CONTROL, head, still_to_be_processed);
1423 pips_debug(2,
"Cycle %p with statement %s depends on:\n",
1426 }, cycle_dependencies_map);
1430 pips_debug(2,
"no cycles with dependencies\n");
1435 while(!
ENDP(still_to_be_processed)) {
1440 for(l=still_to_be_processed; !
ENDP(l); ) {
1448 pips_debug(8,
"Process cycle %p with statement %s\n",
1457 cycle_temporary_precondition_map,
1458 ancestor_map, scc_map);
1470 (partition, c_u, ancestor_map, scc_map, fix_point_map,
1471 cycle_temporary_precondition_map, statement_temporary_precondition_map,
1472 e_c_pre, pre, control_postcondition_map);
1482 ENDP(still_to_be_processed));
1493 }, statement_temporary_precondition_map);
1518 bool postcondition_p,
1523 list still_to_be_processed =
NIL;
1528 pips_debug(2,
"Begin for unstructured %p with e_pre=%p:\n", ndu, e_pre);
1541 if(!
ENDP(cannot_be_reached)) {
1551 pips_debug(3,
"Process unreachable nodes in unstructured %p\n", ndu);
1559 }, cannot_be_reached);
1569 if(!is_dag && !postcondition_p) {
1597 while(!
ENDP(still_to_be_processed)) {
1603 pips_debug(5,
"Try forward processing for\n");
1607 for(l=still_to_be_processed; !
ENDP(l); ) {
1612 still_to_be_processed,
1614 control_postcondition_map)) {
1617 ancestor_map, scc_map, partition, fix_point_map, postcondition_p);
1625 if(!
ENDP(still_to_be_processed)) {
1626 pips_assert(
"still_to_be_processed is empty because of the Bourdoncle's restructuring",
1632 if(!is_dag && !postcondition_p) {
1653 pips_assert(
"Partial path transformer pred_tf is defined",
1659 fp_tf = (*transformer_fix_point_operator)(path_tf);
1714 pips_debug(2,
"End for %s of %s %p with entry node %s and with transformer %p\n",
1715 postcondition_p?
"postcondition" :
"transformer",
1716 is_dag?
"dag" :
"cycle", ndu,
1733 bool postcondition_p)
1738 (partition, ndu, ancestor_map, scc_map, fix_point_map, e_pre, n_pre,
1739 control_postcondition_map, postcondition_p,
true);
1753 bool postcondition_p)
1758 (partition, ndu, ancestor_map, scc_map, fix_point_map, e_pre, n_pre,
1759 control_postcondition_map, postcondition_p,
false);
1796 pips_assert(
"Transformer or postcondition is consistent",
1812 pips_assert(
"Transformer or postcondition is consistent",
1825 bool postcondition_p)
1843 postcondition_p?
"postconditions" :
"transformer");
1860 (partition, ndu, ancestor_map, scc_map, fix_point_map,
1861 postcondition_p? pre_u : pre_u_r, postcondition_p? pre : pre_r,
1862 control_postcondition_map, postcondition_p);
1864 if(postcondition_p) {
1869 (partition, ndu, ancestor_map, scc_map, fix_point_map, pre_u, pre,
1870 control_postcondition_map);
1882 postcondition_p?
"Postconditions":
"Path transformer");
1893 u, (
void *) & fcontext,
1899 pips_debug(2,
"Dump fix point map %p:\n", fix_point_map);
1909 pips_debug(2,
"End of fix point map dump\n");
1912 fprintf(stderr,
"No fix point. Empty fix point map\n");
1918 control_postcondition_map));
1924 pips_debug(2,
"End with unstructured postcondition:\n");
2020 }, entry_node, nodes);
2052 "Have you fully restructured your code?\n",
gen_length(succs));
2057 " because property SEMANTICS_ANALYZE_UNSTRUCTURED is not set\n");
2065 (pre_u, pre, u,
true);
2069 pips_assert(
"Postcondition for unstructured is consistent",
2114 pips_debug(8,
"complex: based on transformer\n");
2123 pips_debug(8,
"filtered over approximated precondition holding for any node pre_n:\n");
2166 "May result from an unreachable exit node\n",
2277 }, entry_node, nodes) ;
2287 fp_tf_u = (*transformer_fix_point_operator)(tf_u);
2294 pips_debug(8,
"Result for fix-point fp_tf_u:\n");
2385 "Have you fully restructured your code?\n",
gen_length(succs));
2397 "Have you fully restructured your code?\n",
gen_length(succs));
2409 " because property SEMANTICS_ANALYZE_UNSTRUCTURED is not set\n");
2433 (pre_u, pre, u,
false);
2481 pips_assert(
"Shut up the compiler", t_post_u==t_post_u && pre==pre && u==u);
2483 pips_assert(
"Total precondition for unstructured is consistent",
float a2sf[2] __attribute__((aligned(16)))
USER generates a user error (i.e., non fatal) by printing the given MSG according to the FMT.
int get_int_property(const string)
void free_transformer(transformer p)
transformer copy_transformer(transformer p)
TRANSFORMER.
transformer transformer_dup(transformer t_in)
transformer package - basic routines
void transformer_free(transformer t)
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.
transformer transformer_empty()
Allocate an empty transformer.
bool transformer_internal_consistency_p(transformer t)
Same as above but equivalenced variables should not appear in the argument list or in the predicate b...
bool meaningless_control_p(control c)
Is exported to exploit non-deterministic control flow graphs.
bool control_test_p(control c)
Check that a node is used as a test in a CFG.
control control_to_ancestor(control vertex, hash_table ancestor_map)
If vertex is an ancestor control node from the input control graph, return vertex,...
void bourdoncle_free(unstructured ndu, hash_table ancestor_map, hash_table scc_map)
list bourdoncle_partition(unstructured u, unstructured *p_ndu, hash_table *p_ancestor_map, hash_table *p_scc_map)
bool cycle_head_p(control c, hash_table ancestor_map, hash_table scc_map)
This node is a cycle call site.
unstructured ancestor_cycle_head_to_scc(control a, hash_table scc_map)
scc_map maps either the ancestor node to its scc if the transformers are computed without context,...
unstructured proper_cycle_head_to_scc(control h, hash_table scc_map)
Retrieve a scc_u from its head.
bool false_successors_only_p(control c)
bool true_successors_only_p(control c)
unstructured cycle_head_to_scc(control c, hash_table ancestor_map, hash_table scc_map)
The ancestor of this node is associated to a specific cycle.
bool refine_transformers_p
Transformer recomputation cannot be of real use unless an interprocedural analysis is performed.
list load_cumulated_rw_effects_list(statement)
bool effects_same_action_p(effect, effect)
list EffectsMayUnion(list l1, list l2, bool(*union_combinable_p)(effect, effect))
list EffectsMayUnion(list l1, list l2, union_combinable_p) input : two lists of effects output : a li...
bool get_bool_property(const string)
FC 2015-07-20: yuk, moved out to prevent an include cycle dependency include "properties....
#define chunk_undefined
obsolete
#define CONTROL_MAP(ctl, code, c, list)
Macro to walk through all the controls reachable from a given control node of an unstructured.
void forward_control_map_get_blocs(c, l)
Build recursively the list of all controls forward-reachable from a control of an unstructured.
void control_map_get_blocs(control c, list *l)
Build recursively the list of all controls reachable from a control of an unstructured.
#define FORWARD_CONTROL_MAP(ctl, code, c, list)
Walk through all the controls forward-reachable from a given control node of an unstructured.
void gen_multi_recurse(void *o,...)
Multi recursion visitor function.
void gen_context_multi_recurse(void *o, void *context,...)
Multi-recursion with context function visitor.
bool gen_false(__attribute__((unused)) gen_chunk *unused)
Return false and ignore the argument.
void gen_null(__attribute__((unused)) void *unused)
Ignore the argument.
bool gen_true(__attribute__((unused)) gen_chunk *unused)
Return true and ignore the argument.
#define ENDP(l)
Test if a list is empty.
#define list_undefined_p(c)
Return if a list is undefined.
void gen_remove(list *cpp, const void *o)
remove all occurences of item o from list *cpp, which is thus modified.
int gen_position(const void *item, const list l)
Element ranks are strictly positive as for first, second, and so on.
#define POP(l)
Modify a list pointer to point on the next element of the list.
#define NIL
The empty list (nil in Lisp)
list gen_copy_seq(list l)
Copy a list structure.
size_t gen_length(const list l)
void gen_list_and_not(list *a, const list b)
Compute A = A inter non B:
#define CONS(_t_, _i_, _l_)
List element cell constructor (insert an element at the beginning of a list)
list gen_nconc(list cp1, list cp2)
physically concatenates CP1 and CP2 but do not duplicates the elements
#define CAR(pcons)
Get the value of the first element of a list.
void gen_free_list(list l)
free the spine of the list
bool gen_in_list_p(const void *vo, const list lx)
tell whether vo belongs to lx
#define FOREACH(_fe_CASTER, _fe_item, _fe_list)
Apply/map an instruction block on all the elements of a list.
void * gen_find_eq(const void *item, const list seq)
list gen_append(list l1, const list l2)
int gen_occurences(const void *vo, const list l)
count occurences of vo in l
#define list_undefined
Undefined list definition :-)
#define MAP(_map_CASTER, _map_item, _map_code, _map_list)
Apply/map an instruction block on all the elements of a list (old fashioned)
list gen_full_copy_list(list l)
Copy a list structure with element copy.
test statement_test(statement)
Get the test of a statement.
bool statement_test_p(statement)
string statement_identification(statement)
Like external_statement_identification(), but with internal information, the hexadecimal address of t...
bool continue_statement_p(statement)
Test if a statement is a CONTINUE, that is the FORTRAN nop, the ";" in C or the "pass" in Python....
string safe_statement_identification(statement)
void * hash_get(const hash_table htp, const void *key)
this function retrieves in the hash table pointed to by htp the couple whose key is equal to key.
void hash_put(hash_table htp, const void *key, const void *val)
This functions stores a couple (key,val) in the hash table pointed to by htp.
void hash_update(hash_table htp, const void *key, const void *val)
update key->val in htp, that MUST be pre-existent.
int hash_table_entry_count(hash_table htp)
now we define observers in order to hide the hash_table type...
struct _newgen_struct_control_ * control
#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
#define STATEMENT_ORDERING_UNDEFINED
mapping.h inclusion
#define MAKE_CONTROL_MAPPING()
#define MAKE_STATEMENT_MAPPING()
#define FREE_CONTROL_MAPPING(map)
#define HASH_MAP(k, v, code, ht)
#define HASH_UNDEFINED_VALUE
value returned by hash_get() when the key is not found; could also be called HASH_KEY_NOT_FOUND,...
#define hash_table_undefined
Value of an undefined hash_table.
#define print_transformer(t)
#define unstructured_control
After the modification in Newgen: unstructured = entry:control x exit:control we have create a macro ...
static int init
Maximal value set for Fortran 77.
#define transformer_undefined
#define transformer_undefined_p(x)
#define control_undefined
#define TRANSFORMER(x)
TRANSFORMER.
#define control_predecessors(x)
#define statement_ordering(x)
#define unstructured_undefined
#define statement_domain
newgen_sizeofexpression_domain_defined
#define control_domain
newgen_controlmap_domain_defined
#define CONTROL(x)
CONTROL.
#define transformer_arguments(x)
#define control_successors(x)
#define control_undefined_p(x)
#define unstructured_exit(x)
#define unstructured_undefined_p(x)
#define test_condition(x)
struct _newgen_struct_transformer_ * transformer
#define control_statement(x)
#define statement_undefined_p(x)
transformer statement_to_postcondition(transformer, statement)
end of the non recursive section
int fprintf()
test sc_min : ce test s'appelle par : programme fichier1.data fichier2.data ...
#define semantics_user_warning
transformer precondition_add_condition_information(transformer pre, expression c, transformer context, bool veracity)
context might be derivable from pre as transformer_range(pre) but this is sometimes very computationa...
transformer dag_or_cycle_to_flow_sensitive_postconditions_or_transformers(list partition, unstructured ndu, hash_table ancestor_map, hash_table scc_map, control_mapping fix_point_map, transformer e_pre, transformer n_pre, hash_table control_postcondition_map, bool postcondition_p, bool is_dag)
Should ndu be a dag or a cycle?
static void update_control_postcondition(control c, transformer post, control_mapping control_postcondition_map)
static list get_cycle_dependencies(control d, control_mapping cycle_dependencies_map)
Some cycle may appear nowhere but in the DAG and have no entries in the table.
transformer cycle_to_flow_sensitive_postconditions_or_transformers(list partition, unstructured ndu, hash_table ancestor_map, hash_table scc_map, control_mapping fix_point_map, transformer e_pre, transformer n_pre, hash_table control_postcondition_map, bool postcondition_p)
Compute transformers or preconditions.
transformer load_statement_temporary_precondition(statement s, statement_mapping statement_temporary_precondition_map)
transformer unstructured_to_flow_sensitive_postconditions(transformer pre_u, transformer pre, unstructured u)
compute pre- and post-conditions in an unstructured from the entry precondition pre and return the ex...
static void store_control_postcondition(control c, transformer post, control_mapping control_postcondition_map)
static control_mapping free_control_postcondition_map(control_mapping control_postcondition_map)
static control_mapping make_control_postcondition_map()
static void cycle_to_flow_sensitive_preconditions(list partition, unstructured c_u, hash_table ancestor_map, hash_table scc_map, control_mapping fix_point_map, control_mapping cycle_temporary_precondition_map, statement_mapping statement_temporary_precondition_map, transformer c_pre, transformer pre, control_mapping control_postcondition_map)
Very likely the transformer paths wrt the entry point and not really a postcondition.
void print_statement_temporary_precondition(statement_mapping statement_temporary_precondition_map)
static control_mapping free_control_fix_point_map(control_mapping control_fix_point_map)
transformer load_cycle_fix_point(control c, hash_table fix_point_map)
transformer unstructured_to_postcondition(transformer pre, unstructured u, transformer tf)
transformer load_cycle_temporary_precondition(control c, control_mapping cycle_temporary_precondition_map, hash_table ancestor_map, hash_table scc_map __attribute__((__unused__)))
static void unreachable_node_to_transformer(control c)
static control_mapping make_control_fix_point_map()
static void local_process_unreachable_node(control c, recursive_context *pcontext)
transformer unstructured_to_transformer(unstructured u, transformer e_pre, list e)
effects of u
void update_temporary_precondition(void *k, transformer pre, hash_table precondition_map)
static transformer load_arc_precondition(control, control, control_mapping)
forward declaration
static list unstructured_to_effects(unstructured scc, hash_table ancestor_map, hash_table scc_map)
In fact, non-deterministic unstructured to effects.
void update_statement_temporary_precondition(statement s, transformer pre, statement_mapping statement_temporary_precondition_map)
transformer unstructured_to_flow_sensitive_total_preconditions(transformer t_post_u, transformer pre, unstructured u)
static void process_ready_node(control c, transformer pre_entry, transformer n_pre, unstructured u, control_mapping control_postcondition_map, hash_table ancestor_map, hash_table scc_map, list partition, control_mapping fix_point_map, bool postcondition_p)
static transformer unstructured_to_postconditions(transformer pre, transformer pre_first, unstructured u)
static void store_control_fix_point(control c, transformer fptf, control_mapping control_fix_point_map)
transformer unstructured_to_flow_insensitive_transformer(unstructured u)
This simple fix-point over-approximates the CFG by a fully connected graph.
static bool ready_to_be_processed_p(control c, list to_be_processed, list still_to_be_processed, list already_processed, control_mapping control_postcondition_map)
a control is ready to be processed if all its predecessors have known postconditions or can receive a...
static void dag_to_flow_sensitive_preconditions(list partition, unstructured ndu, hash_table ancestor_map, hash_table scc_map, control_mapping fix_point_map, transformer pre_u, transformer pre, control_mapping control_postcondition_map)
void update_cycle_temporary_precondition(control c, transformer pre, control_mapping cycle_temporary_precondition_map)
static void remove_cycle_dependencies(control c, control_mapping cycle_dependencies_map)
c has been processed and no other cycle can depend on it
static list non_deterministic_unstructured_to_effects(unstructured scc, hash_table ancestor_map, hash_table scc_map)
static transformer get_control_precondition(control c, control_mapping control_postcondition_map, unstructured u, transformer pre_entry)
transformer unstructured_to_flow_sensitive_postconditions_or_transformers(transformer pre_u, transformer pre, unstructured u, bool postcondition_p)
compute either the postconditions in an unstructured or the transformer of this unstructured.
static transformer load_control_fix_point(control c, control_mapping control_fix_point_map, hash_table ancestor_map, hash_table scc_map)
The fix point can be linked either to the entry node of the scc or to the ancestor node.
transformer dag_to_flow_sensitive_postconditions_or_transformers(list partition, unstructured ndu, hash_table ancestor_map, hash_table scc_map, control_mapping fix_point_map, transformer e_pre, transformer n_pre, hash_table control_postcondition_map, bool postcondition_p)
Compute transformers or preconditions.
static transformer load_control_postcondition(control c, control_mapping control_postcondition_map)
static void print_control_node_unss_sem(list l)
static void print_control_node_uns(control c)
semantical analysis
static void print_cycle_head_to_fixpoint(control c, recursive_context *pcontext)
A debug function to prettyprint the fix points.
static void add_cycle_dependency(control d, control c, control_mapping cycle_dependencies_map)
State that d depends on c: cycle c must be processed before cycle d can be processed.
static void unstructured_to_transformers(unstructured u, transformer pre)
Computation of transformers associated to each node of u and to each of its sub-statements.
void print_control_postcondition_map(control_mapping control_postcondition_map)
unstructured.c
static void node_to_path_transformer_or_postcondition(control c, recursive_context *pcontext)
A debug function to prettyprint the result.
static bool process_unreachable_node(control c, control_mapping control_postcondition_map, bool postcondition_p)
transformer load_statement_precondition(statement)
transformer load_statement_transformer(statement)
The structure used to build lists in NewGen.