6 #ifndef semantics_header_included
7 #define semantics_header_included
34 #define SEMANTICS_OPTIONS "?Otcfieod-D:"
36 #define SEQUENTIAL_TRANSFORMER_SUFFIX ".tran"
37 #define USER_TRANSFORMER_SUFFIX ".utran"
38 #define SEQUENTIAL_PRECONDITION_SUFFIX ".prec"
39 #define USER_PRECONDITION_SUFFIX ".uprec"
40 #define SEQUENTIAL_TOTAL_PRECONDITION_SUFFIX ".tprec"
41 #define USER_TOTAL_PRECONDITION_SUFFIX ".utprec"
50 #if defined(__STDC_VERSION__) && (__STDC_VERSION__ >= 199901L)
51 #define semantics_user_warning(...) \
52 semantics_user_warning_func(CURRENT_FUNCTION, __VA_ARGS__)
54 #define semantics_user_warning semantics_user_warning_func2
struct _newgen_struct_statement_ * statement
bool print_code_as_a_graph_preconditions(const string)
void integer_value_and_precondition_to_integer_interval(entity, transformer, int *, int *)
Should be used by previous function, integer_expression_and_precondition_to_integer_interval()
list load_body_effects(entity)
void print_control_postcondition_map(control_mapping)
unstructured.c
void free_postcondition_map(void)
bool print_source_transformers(const char *)
transformer call_to_transformer(call, transformer, list)
Use to be static, but may be called from expressions in C.
bool print_call_graph_with_transformers(const string)
transformer complete_non_identity_statement_transformer(transformer, transformer, statement)
FI: only implemented for while loops.
void update_statement_precondition(statement, transformer)
transformer any_update_to_transformer(entity, list, list, transformer)
precondition
transformer transformer_add_domain_condition(transformer, expression, transformer, bool)
transformer declarations_to_transformer(list, transformer)
For C declarations.
list variables_to_old_values(list)
bool old_summary_precondition(char *)
transformer precondition_filter_old_values(transformer)
void reset_call_site_number(void)
transformer substitute_stubs_in_transformer(transformer, call, statement, bool)
Exploit the binding map to substitute calles's stubs by actual arguments, which may be stubs of the c...
transformer cycle_to_flow_sensitive_postconditions_or_transformers(list, unstructured, hash_table, hash_table, control_mapping, transformer, transformer, hash_table, bool)
Compute transformers or preconditions.
transformer load_cycle_temporary_precondition(control, control_mapping, hash_table, hash_table)
transformer load_completed_statement_transformer(statement)
three mappings used throughout semantics analysis:
transformer struct_variable_equality_to_transformer(entity, type, expression, transformer, list)
transformer integer_expression_to_transformer(entity, expression, transformer, bool)
Do check wrt to value mappings...
transformer unstructured_to_transformer(unstructured, transformer, list)
effects of u
transformer whileloop_to_k_transformer(whileloop, transformer, list, int)
void update_summary_precondition_in_declaration(expression, transformer)
This function is called to deal with call sites located in initialization expressions carried by decl...
void delete_statement_transformer(statement)
transformer transformer_apply_field_assignments_or_equalities(transformer, reference, reference, type, bool)
For all analyzable fields f, apply the assignment "le.f = re.f;" to transformer t.
transformer loop_to_initialization_transformer(loop, transformer)
Transformer expression the loop initialization.
unsigned int number_of_usable_functional_parameters(list)
Number of formal parameters in pl before a vararg is reached.
transformer transformer_add_loop_index_initialization(transformer, loop, transformer)
The loop initialization is performed before tf.
void transformer_add_type_information(transformer)
type.c
bool transformer_map_undefined_p(void)
dbm_interface.c
bool path_transformer(const string)
void integer_expression_and_precondition_to_integer_interval(expression, transformer, int *, int *)
Could be used for bool expressions too? Extended to any kind of expression?
transformer loop_to_continue_transformer(loop, transformer)
transformer get_module_precondition(entity)
interprocedural.c
void make_total_precondition_map(void)
transformer any_conditional_to_transformer(entity, list, transformer)
Take care of the returned value.
transformer unstructured_to_flow_sensitive_total_preconditions(transformer, transformer, unstructured)
transformer any_expression_side_effects_to_transformer(expression, transformer, bool)
transformer unstructured_to_flow_sensitive_postconditions(transformer, transformer, unstructured)
compute pre- and post-conditions in an unstructured from the entry precondition pre and return the ex...
transformer transformer_intra_to_inter(transformer, list)
bool print_source_total_preconditions(const char *)
bool refine_transformers(char *)
transformer load_statement_temporary_precondition(statement, statement_mapping)
list semantics_expression_to_points_to_sinks(expression)
Returns a list of cells.
void make_postcondition_map(void)
void set_prettyprint_transformer(void)
void update_statement_semantic(statement, transformer)
transformer any_assign_to_transformer(list, list, transformer)
precondition
void delete_statement_semantic(statement)
void add_implicit_interprocedural_write_effects(entity, list)
It is assumed that al is an abstract location that is written and which may conflict with effects in ...
bool statement_semantic_undefined_p(statement)
transformer complete_whileloop_transformer(transformer, transformer, whileloop)
FI: I'm not sure this function is useful.
bool program_postcondition(const string)
The program correctness postcondition cannot be infered.
list load_module_intraprocedural_effects(entity)
transformer safe_any_expression_to_transformer(entity, expression, transformer, bool)
Always return a usable transformer.
transformer substitute_formal_array_elements_in_precondition(transformer, entity, list, transformer, list)
transformer path_transformer_on(statement, path, path, int)
text get_text_preconditions(const string)
transformer any_scalar_assign_to_transformer(entity, expression, list, transformer)
precondition
transformer precondition_intra_to_inter(entity, transformer, list)
transformer expression_effects_to_transformer(expression)
list declaration_to_transformer_list(entity, transformer)
ri_to_transformer_lists.c
list safe_assigned_expression_to_transformer_list(entity, expression, transformer)
Always returns a fully defined transformer.
transformer integer_assign_to_transformer(expression, expression, transformer, list)
This function never returns an undefined transformer.
bool value_mappings_compatible_vector_p(Pvecteur)
transform a vector based on variable entities into a vector based on new value entities when possible...
bool transformers_intra_full(char *)
transformer any_user_call_site_to_transformer(entity, list, transformer, list)
bool print_icfg_with_loops_total_preconditions(const string)
bool statement_weakly_feasible_p(statement)
utils.c
void set_module_global_arguments(list)
bool transformers_intra_fast(char *)
Functions to make transformers.
transformer load_statement_semantic(statement)
transformer load_cycle_fix_point(control, hash_table)
bool statement_strongly_feasible_p(statement)
Return true if statement s is reachable according to its precondition.
void add_declaration_list_information(transformer, list, bool)
transformer any_loop_to_transformer(transformer, transformer, transformer, statement, list, transformer)
bool preconditions_inter_fast(char *)
transformer c_user_call_to_transformer(entity, list, transformer, list)
list any_scalar_assign_to_transformer_list(entity, expression, list, transformer)
precondition
sentence make_pred_commentary_sentence(string, string)
sentence make_pred_commentary_sentence(string str_pred, string comment_prefix) input : a substring fo...
bool non_empty_range_wrt_precondition_p(range, transformer)
transformer load_statement_precondition(statement)
bool transformers_inter_full(char *)
transformer simple_affine_to_transformer(entity, Pvecteur, bool)
INTEGER EXPRESSIONS.
void free_total_precondition_map(void)
text text_for_a_transformer(transformer, bool)
call this one from outside.
transformer generic_substitute_formal_array_elements_in_transformer(transformer, entity, list, transformer, list, bool)
transformer any_loop_to_postcondition(statement, transformer, transformer, transformer, transformer, transformer, transformer, transformer, transformer, transformer)
list load_summary_effects(entity)
FI->FI, FI->BC: these two functions should be moved into effects-util or effects-simple.
bool summary_total_postcondition(char *)
transformer add_index_range_conditions(transformer, entity, range, transformer)
transformer substitute_scalar_stub_in_transformer(transformer, entity, entity, bool, list *)
If both "se", source entity, and "de", destination entity, are defined, substitute the values of "se"...
transformer loop_bound_evaluation_to_transformer(loop, transformer)
Side effects in loop bounds and increment are taken into account.
transformer forloop_to_postcondition(transformer, forloop, transformer)
transformer transformer_logical_inequalities_add(transformer, entity)
PROCESSING OF LOGICAL EXPRESSIONS.
list declarations_to_transformer_list(list, transformer)
For C declarations.
bool print_initial_precondition(const string)
bool print_icfg_with_preconditions(const string)
transformer any_scalar_assign_to_transformer_without_effect(entity, expression, transformer)
assign to the scalar variable v the expression rhs (a scalar variable has a basic type; it cannot be ...
void translate_global_value(entity, transformer, entity)
Try to convert an value on a non-local variable into an value on a local variable using a guessed nam...
void set_total_precondition_map(statement_mapping)
transformer any_expressions_side_effects_to_transformer(list, transformer, bool)
same as any_expression_side_effects_to_transformer() but for a list of expressions
transformer tf_equivalence_equalities_add(transformer)
mappings.c
bool preconditions_inter_full_with_points_to(char *)
bool refine_transformers_p
Transformer recomputation cannot be of real use unless an interprocedural analysis is performed.
transformer generic_complete_statement_transformer(transformer, transformer, statement, bool)
Loops, do, for, while or repeat, have transformers linked to their body preconditions so as to comput...
list any_update_to_transformer_list(entity, list, list, transformer)
precondition
void transformer_add_reference_information(transformer, statement)
list variables_to_values(list)
transformer modulo_by_a_constant_to_transformer(entity, transformer, entity, int)
Analyze v2 % k, with v2 constrainted by tf, assuming tf is a precondition.
transformer declaration_to_transformer(entity, transformer)
Note: initializations of static variables are not used as transformers but to initialize the program ...
transformer intrinsic_to_transformer(entity, list, transformer, list)
effects of intrinsic call
void make_semantic_map(void)
void update_statement_postcondition(statement, transformer)
transformer user_function_call_to_transformer(entity, expression, transformer)
a function call is a call to a non void function in C and to a FUNCTION in Fortran
void store_statement_semantic(statement, transformer)
list complete_any_loop_transformer_list(transformer, transformer, transformer, transformer, transformer, transformer)
FI: used to be complete_any_loop_transformer() with a direct reduction by convex hull.
list complete_repeatloop_transformer_list(transformer, transformer, whileloop)
transformer new_substitute_stubs_in_transformer(transformer, call, statement, bool)
bool precondition_minmax_of_value(entity, transformer, intptr_t *, intptr_t *)
compute integer bounds pmax, pmin of value val under preconditions tr require value mappings set !
void add_module_call_site_precondition(entity, transformer)
transformer propagate_preconditions_in_declarations(list, transformer, void(*)(expression, transformer))
This function is mostly copied from declarations_to_transformer().
bool semantics_usable_points_to_reference_p(reference, expression, int)
See if references rlhs is usable and process null, undefined and anywhere locations defined by rlhs.
transformer transformer_apply_unknown_field_equalities(transformer, reference, type)
bool refine_transformers_with_points_to(char *)
bool false_condition_wrt_precondition_p(expression, transformer)
bool precondition_minmax_of_expression(expression, transformer, intptr_t *, intptr_t *)
compute integer bounds pmax, pmin of expression exp under preconditions tr require value mappings set...
bool print_icfg_with_total_preconditions(const string)
list effects_to_arguments(list)
list of effects
bool module_name_to_preconditions(const char *)
resource module_name_to_preconditions(char * module_name): compute a transformer for each statement o...
transformer transformer_apply_field_equalities(transformer, reference, reference, type)
int dynamic_call_count(entity)
list any_basic_update_to_transformer_list(entity, list, list, transformer)
precondition
void reset_total_precondition_map(void)
transformer transformer_add_any_relation_information(transformer, entity, expression, expression, transformer, bool, bool)
compute transformer or precondition
void free_semantic_map(void)
transformer pointer_expression_to_transformer(entity, expression, transformer, bool)
bool true_condition_wrt_precondition_p(expression, transformer)
void translate_global_values(entity, transformer)
statement_mapping compute_postcondition(statement, statement_mapping, statement_mapping)
statement_mapping compute_postcondition(stat, post_map, pre_map) statement stat; statement_mapping po...
list any_assign_to_transformer_list(list, list, transformer)
precondition
bool precondition_map_undefined_p(void)
list new_complete_whileloop_transformer_list(transformer, transformer, whileloop, bool)
transformer complete_any_loop_transformer(transformer, transformer, transformer, transformer, transformer, transformer, transformer, transformer)
bool test_warning_counters(void)
void cumulated_effects_map_print(void)
ca n'a rien a` faire ici, et en plus, il serait plus inte'ressant d'avoir une fonction void statement...
bool print_code_transformers(const char *)
bool transformers_inter_fast(char *)
bool empty_range_wrt_precondition_p(range, transformer)
A range cannot be tested exactly wrt a precondition You can try to prove that it is empty or you can ...
transformer statement_to_total_precondition(transformer, statement)
ri_to_total_preconditions.c
void add_or_kill_equivalenced_variables(entity, bool)
Look for variables equivalenced with e.
bool use_points_to_p(void)
transformer add_loop_index_exit_value(transformer, loop, transformer)
The exit value is known if.
transformer safe_any_assign_operation_to_transformer(entity, list, transformer, bool)
bool program_precondition(const string)
Compute the union of all initial preconditions.
void update_temporary_precondition(void *, transformer, hash_table)
bool total_precondition_map_undefined_p(void)
transformer new_add_formal_to_actual_bindings(call, transformer, entity)
Take side effects into account:
transformer new_array_elements_backward_substitution_in_transformer(transformer, entity, type, expression, transformer, list)
bool print_call_graph_with_preconditions(const string)
void expressions_to_summary_precondition(transformer, list)
bool postcondition_map_undefined_p(void)
postcondition.c
transformer expression_to_transformer(expression, transformer, list)
Just to capture side effects as the returned value is ignored.
void set_warning_counters(void)
transformer loop_initialization_to_transformer(loop, transformer)
Note: It used to be implemented by computing the effect list of the lower bound expression and and ne...
transformer repeatloop_to_transformer(whileloop, transformer, list)
effects of whileloop wl
void call_to_summary_precondition(transformer, call)
transformer all_data_to_precondition(entity)
any variable is included.
bool print_call_graph_with_total_preconditions(const string)
list loop_to_transformer_list(loop, transformer, list)
void store_statement_transformer(statement, transformer)
list statement_to_transformer_list(statement, transformer)
A transformer is already available for statement s, but it is going to be refined into a list of tran...
transformer dag_or_cycle_to_flow_sensitive_postconditions_or_transformers(list, unstructured, hash_table, hash_table, control_mapping, transformer, transformer, hash_table, bool, bool)
Should ndu be a dag or a cycle?
transformer safe_expression_to_transformer(expression, transformer)
bool statement_total_precondition_undefined_p(statement)
void set_semantic_map(statement_mapping)
transformer load_statement_total_precondition(statement)
bool summary_transformer(char *)
transformer new_array_elements_substitution_in_transformer(transformer, entity, type, expression, transformer, list, bool)
int get_call_site_number(void)
transformer new_array_element_backward_substitution_in_transformer(transformer, entity, reference, reference)
Substitute formal location entity l by a location entity corresponding to ar, if it is possible.
transformer forloop_to_transformer(forloop, transformer, list)
effects of forloop fl
void set_transformer_map(statement_mapping)
bool eval_condition_wrt_precondition_p(expression, transformer, bool)
bool print_icfg_with_control_preconditions(const string)
void update_statement_total_precondition(statement, transformer)
void free_precondition_map(void)
bool check_range_wrt_precondition(range, transformer, bool)
FI: this function is outdated because it does not compute the transformers for the range expressions,...
list effects_to_entity_list(list)
returns an allocated list of entities that appear in lef.
transformer unstructured_to_postcondition(transformer, unstructured, transformer)
transformer load_statement_transformer(statement)
transformer struct_reference_equality_to_transformer(reference, type, expression, transformer, list)
bool preconditions_intra(char *)
transformer transformer_apply_unknown_field_assignments(transformer, reference, type)
void precondition_add_type_information(transformer)
void reset_precondition_map(void)
transformer complete_loop_transformer(transformer, transformer, loop)
The transformer computed and stored for a loop is useful to compute the loop body precondition,...
bool preconditions_inter_full(char *)
transformer affine_increment_to_transformer(entity, Pvecteur)
transformer new_array_elements_forward_substitution_in_transformer(transformer, entity, type, expression, transformer, list)
transformer old_complete_whileloop_transformer(transformer, transformer, whileloop)
transformer add_loop_skip_condition(transformer, loop, transformer)
tf and pre are a unique data structure when preconditions are computed
void make_precondition_map(void)
bool print_program_precondition(const string)
void expression_to_summary_precondition(transformer, expression)
transformer load_summary_transformer(entity)
list forloop_to_transformer_list(forloop, transformer, list)
bool preconditions_intra_fast(char *)
transformer safe_assigned_expression_to_transformer(entity, expression, transformer)
Always returns a fully defined transformer.
int simplify_boolean_expression_with_precondition(expression, transformer)
Simplification of bool expressions with precondition.
text get_text_total_preconditions(const string)
transformer user_call_to_transformer(entity, list, transformer, list)
transformer float_expression_to_transformer(entity, expression, transformer, bool)
transformer new_complete_whileloop_transformer(transformer, transformer, whileloop, bool)
entered_p is used to for the execution of at least one iteration
transformer substitute_formal_array_elements_in_transformer(transformer, entity, list, transformer, list)
bool print_code_total_preconditions(const char *)
void delete_statement_precondition(statement)
transformer condition_to_transformer(expression, transformer, bool)
To capture side effects and to add C twist for numerical conditions.
statement_mapping get_postcondition_map(void)
bool total_preconditions_inter(char *)
transformer logical_expression_to_transformer(entity, expression, transformer, bool)
Could be used to compute preconditions too.
transformer standard_whileloop_to_transformer(whileloop, transformer, list)
This function computes the effect of K loop iteration, with K positive.
transformer dimensions_to_transformer(entity, transformer)
Assumes that entity_has_values_p(v) holds.
transformer any_expression_to_transformer(entity, expression, transformer, bool)
A set of functions to compute the transformer associated to an expression evaluated in a given contex...
bool statement_transformer_undefined_p(statement)
bool print_icfg_with_control_transformers(const string)
transformer compute_path_transformer(statement, path, path)
transformer assigned_expression_to_transformer(entity, expression, transformer)
transformer assigned_expression_to_transformer(entity e, expression expr, list ef): returns a transfo...
transformer generic_transformer_intra_to_inter(transformer, list, bool)
transformer translation from the module intraprocedural transformer to the module interprocedural tra...
bool interprocedural_summary_precondition_with_points_to(char *)
transformer lhs_expression_to_transformer(entity, expression, transformer)
This function deals with e1.e2 and e1->e2, not with simple references such as x or a[i].
bool same_analyzable_type_scalar_entity_list_p(list)
void free_transformer_map(void)
list intrinsic_to_transformer_list(entity, list, transformer, list)
because of the conditional and the comma C intrinsics at least
list complete_whileloop_transformer_list(transformer, transformer, whileloop)
list get_module_global_arguments(void)
ri_to_preconditions.c
transformer whileloop_to_transformer(whileloop, transformer, list)
effects of whileloop l
transformer whileloop_to_postcondition(transformer, whileloop, transformer)
transformer logical_not_to_transformer(entity, list, transformer)
returns the transformer associated to a C logical not, !, applied to an integer argument,...
transformer loop_to_enter_transformer(loop, transformer)
Transformer expressiong the conditions between the index and the loop bounds according to the sign of...
transformer loop_to_transformer(loop, transformer, list)
The transformer associated to a DO loop does not include the exit condition because it is used to com...
transformer any_basic_update_to_transformer(entity, list, list, transformer)
precondition
transformer safe_integer_expression_to_transformer(entity, expression, transformer, bool)
Always return a defined transformer, using effects in case a more precise analysis fails.
transformer conditional_to_transformer(expression, expression, expression, transformer, list)
FI: not too smart to start with the special case with no value returned, just side-effects....
list integer_assign_to_transformer_list(expression, expression, transformer, list)
This function never returns an undefined transformer.
transformer value_passing_summary_transformer(entity, transformer)
With value passing, writes on formal parameters are not effective interprocedurally unless an array i...
void simplify_minmax_expression(expression, transformer)
tries hard to simplify expression e if it is a min or a max operator, by evaluating it under precondi...
text get_text_transformers(const string)
void set_postcondition_map(statement_mapping)
void set_precondition_map(statement_mapping)
void update_statement_transformer(statement, transformer)
void expression_and_precondition_to_integer_interval(expression, transformer, int *, int *)
Evaluate expression e in context p, assuming that e is an integer expression.
void reset_semantic_map(void)
transformer safe_any_expression_side_effects_to_transformer(expression, transformer, bool)
Same as any_expression_side_effects_to_transformer() but effects are used to always generate a transf...
statement_mapping get_semantic_map(void)
transformer expressions_to_transformer(list, transformer)
Compute the transformer associated to a list of expressions such as "i=0, j = 1;".
bool print_source_preconditions(const char *)
transformer any_expressions_to_transformer(entity, list, transformer)
Compute the transformer associated to a list of expressions such as "i=0, j = 1;".
list dynamic_variables_to_values(list)
Build the list of values to be projected when the declaration list list_mod is no longer valid becaus...
void module_to_value_mappings(entity)
void module_to_value_mappings(entity m): build hash tables between variables and values (old,...
transformer load_summary_precondition(entity)
summary_preconditions are expressed in any possible frame, in fact the frame of the last procedure th...
void store_statement_precondition(statement, transformer)
void precondition_add_reference_information(transformer, statement)
void upwards_vect_rename(Pvecteur, transformer)
Renaming of variables in v according to transformations occuring later.
bool generic_module_name_to_transformers(const char *, bool)
bool generic_module_name_to_transformers(char * module_name, bool in_context): compute a transformer ...
transformer load_summary_total_postcondition(entity)
summary_preconditions are expressed in any possible frame, in fact the frame of the last procedure th...
transformer effects_to_transformer(list)
list of effects
transformer new_whileloop_to_transformer(whileloop, transformer, list)
effects of whileloop wl
void store_statement_postcondition(statement, transformer)
bool print_code_preconditions(const char *)
bool print_icfg_with_loops_transformers(const string)
transformer c_return_to_transformer(entity, list, list, transformer)
transformer complete_repeatloop_transformer(transformer, transformer, whileloop)
transformer statement_to_postcondition(transformer, statement)
end of the non recursive section
text words_predicate_to_commentary(list, string)
text words_predicate_to_commentary(list w_pred, string comment_prefix) input : a list of strings,...
void print_statement_temporary_precondition(statement_mapping)
transformer add_formal_to_actual_bindings(call, transformer, entity)
add_formal_to_actual_bindings(call c, transformer pre, entity caller):
transformer assign_operation_to_transformer(entity, expression, expression, transformer)
Returns an undefined transformer in case of failure.
void make_transformer_map(void)
bool total_preconditions_intra(char *)
transformer filter_transformer(transformer, list)
Previous version of effects_to_transformer() transformer effects_to_transformer(list e) { list args =...
bool module_name_to_transformers_in_context(const char *)
bool intraprocedural_summary_precondition(char *)
transformer repeatloop_to_postcondition(transformer, whileloop, transformer)
statement_mapping get_total_precondition_map(void)
transformer unstructured_to_flow_sensitive_postconditions_or_transformers(transformer, transformer, unstructured, bool)
compute either the postconditions in an unstructured or the transformer of this unstructured.
bool interprocedural_summary_precondition(char *)
transformer transformer_apply_field_assignments(transformer, reference, reference, type)
bool module_name_to_total_preconditions(const char *)
void update_summary_precondition(entity, transformer)
void update_summary_precondition(e, t): t is supposed to be a precondition related to one of e's call...
void delete_statement_postcondition(statement)
transformer complete_forloop_transformer(transformer, transformer, forloop)
transformer any_assign_operation_to_transformer(entity, list, transformer, bool)
text text_transformer(transformer)
text text_transformer(transformer tran) input : a transformer representing a transformer or a precond...
bool module_name_to_transformers(const char *)
bool print_icfg_with_loops_preconditions(const string)
bool print_code_as_a_graph_total_preconditions(const string)
transformer transformer_add_integer_relation_information(transformer, entity, expression, expression, bool, bool)
It is supposed to be obsolete but is still called.
transformer dag_to_flow_sensitive_postconditions_or_transformers(list, unstructured, hash_table, hash_table, control_mapping, transformer, transformer, hash_table, bool)
Compute transformers or preconditions.
transformer transformer_add_condition_information(transformer, expression, transformer, bool)
bool summary_precondition(char *)
transformer array_elements_substitution_in_transformer(transformer, entity, type, expression, transformer, list, bool)
transformer transformer_add_loop_index_incrementation(transformer, loop, transformer)
void add_intraprocedural_value_entities(entity)
Use to be static, but may be called from ri_to_transformer.
void reset_postcondition_map(void)
transformer points_to_unary_operation_to_transformer(entity, entity, expression, transformer, bool, bool)
This function is redundant with generic_unary_operation_to_transformer() except for its use of parame...
text call_site_to_module_precondition_text(entity, entity, statement, call)
This function does everything needed.
bool statement_postcondition_undefined_p(statement)
transformer statement_to_transformer(statement, transformer)
stmt precondition
transformer affine_to_transformer(entity, Pvecteur, bool)
bool check_condition_wrt_precondition(expression, transformer, bool)
transformer apply_array_effect_to_transformer(transformer, effect, bool)
ri_to_transformers.c
transformer substitute_struct_stub_in_transformer(transformer, reference, type, reference, type, bool, list *)
transformer transformer_formal_parameter_projection(entity, transformer)
transformer whileloop_to_total_precondition(transformer, whileloop, transformer, transformer)
bool statement_precondition_undefined_p(statement)
transformer any_loop_to_k_transformer(transformer, transformer, transformer, statement, list, transformer, int)
loop.c
transformer struct_variable_assignment_to_transformer(entity, type, expression, transformer, list)
list module_to_formal_analyzable_parameters(entity)
returns a module's parameter's list
transformer data_to_precondition(entity)
restricted to variables with effects.
list semantics_expression_to_points_to_sources(expression)
points_to.c
transformer new_whileloop_to_k_transformer(whileloop, transformer, list, int)
list complete_forloop_transformer_list(transformer, transformer, forloop)
void transformer_add_variable_type_information(transformer, entity)
text semantic_to_text(entity, int, statement)
this function name is VERY misleading - it should be changed, sometime FI
void semantics_user_warning_func(const char *, const char *,...)
void path_initialize(statement, statement, statement, path *, path *)
path_transformer.c
void variables_to_new_values(Pvecteur)
replace variables by new values which is necessary for equivalenced variables
void update_statement_temporary_precondition(statement, transformer, statement_mapping)
transformer transformer_add_range_condition(transformer, expression, transformer, bool)
transformer string_expression_to_transformer(entity, expression)
bool condition_true_wrt_precondition_p(expression, transformer)
A condition cannot be tested exactly wrt a precondition You can try to prove that it is always true (...
void update_cycle_temporary_precondition(control, transformer, control_mapping)
transformer unstructured_to_flow_insensitive_transformer(unstructured)
This simple fix-point over-approximates the CFG by a fully connected graph.
bool summary_total_precondition(char *)
transformer new_loop_to_transformer(loop, transformer, list)
loop_to_transformer() was developed first but is not as powerful as the new algorithm used for all ki...
bool transformers_inter_full_with_points_to(char *)
transformer logical_intrinsic_to_transformer(entity, call, transformer, bool)
list variable_to_values(entity)
transformer bitwise_xor_to_transformer(entity, list, transformer)
returns the transformer associated to a C bitwise xor, ^, applied to two integer argument,...
transformer complete_statement_transformer(transformer, transformer, statement)
Returns the effective transformer ct for a given statement s.
bool print_code_as_a_graph_transformers(const string)
int call_site_count(entity)
cproto-generated files
statement_mapping get_transformer_map(void)
void delete_statement_total_precondition(statement)
bool simple_dead_loop_p(expression, expression)
void reset_transformer_map(void)
list complete_loop_transformer_list(transformer, transformer, loop)
bool print_icfg_with_transformers(const string)
statement_mapping get_precondition_map(void)
transformer precondition_add_condition_information(transformer, expression, transformer, bool)
context might be derivable from pre as transformer_range(pre) but this is sometimes very computationa...
transformer fortran_user_call_to_transformer(entity, list, list)
Effects are necessary to clean up the transformer t_caller.
bool statement_feasible_p(statement)
Return true if statement s is reachable according to its precondition.
transformer load_statement_postcondition(statement)
bool semantic_map_undefined_p(void)
prettyprint.c
bool condition_false_wrt_precondition_p(expression, transformer)
void semantics_user_warning_func2(const char *,...)
bool initial_precondition(string)
initial.c
void add_equivalenced_values(entity, entity, bool)
transformer generic_reference_to_transformer(entity, reference, transformer, bool)
expression.c
void store_statement_total_precondition(statement, transformer)
text string_predicate_to_commentary(string, string)
text string_predicate_to_commentary(string str_pred, string comment_prefix) input : a string,...
transformer any_basic_update_operation_to_transformer(entity, entity, entity)
See also any_basic_update_to_transformer(), which should be based on this function.
bool print_icfg_with_control_total_preconditions(const string)
transformer struct_reference_assignment_to_transformer(reference, type, expression, transformer, list)
transformer update_precondition_with_call_site_preconditions(transformer, entity, entity)
Update precondition t for callee with preconditions of call sites to callee in caller.
list assigned_expression_to_transformer_list(entity, expression, transformer)
transformer assigned_expression_to_transformer(entity e, expression expr, list ef): returns a transfo...
transformer loop_to_total_precondition(transformer, loop, transformer, transformer)
transformer loop_to_postcondition(transformer, loop, transformer)
le type des coefficients dans les vecteurs: Value est defini dans le package arithmetique
The structure used to build lists in NewGen.
1.9.1