+
+ // Examine all relations for this variable (scan the list)
+ // The contribute of each relation will be intersected (logical and)
+ while (relation != NULL) {
+ context->current_relation = relation;
+
+ if (TRACE_ABC_REMOVAL) {
+ printf ("Processing (%d): ", variable);
+ print_summarized_value_relation (relation);
+ printf ("\n");
+ }
+
+ // We decie what to do according the the type of the related value
+ switch (relation->related_value.type) {
+ case MONO_ANY_SUMMARIZED_VALUE:
+ // No added information, skip it
+ break;
+ case MONO_CONSTANT_SUMMARIZED_VALUE:
+ // Intersect range with constant (taking into account the relation)
+ intersect_value (&(context->ranges.zero), relation->related_value.value.constant.value, relation->relation);
+ break;
+ case MONO_VARIABLE_SUMMARIZED_VALUE:
+ // Generally, evaluate related variable and intersect ranges.
+ // However, some check is necessary...
+
+ // If the relation is "ANY", nothing to do (no added information)
+ if (relation->relation != MONO_ANY_RELATION) {
+ int related_variable = relation->related_value.value.variable.variable;
+ MonoRelationsEvaluationContext *related_context = &(area->contexts [related_variable]);
+
+ // The second condition in the "or" avoids messing with "back edges" in the graph traversal
+ // (they are simply ignored instead of triggering the handling of recursion)
+ if ( (related_context->status == MONO_RELATIONS_EVALUATION_NOT_STARTED) || !
+ ((related_context->current_relation->related_value.type == MONO_VARIABLE_SUMMARIZED_VALUE) &&
+ (related_context->current_relation->related_value.value.variable.variable == variable))) {
+ // Evaluate the related variable
+ evaluate_relation_with_target_variable (area, related_variable, target_variable, context);
+
+ // Check if we are part of a recursive loop
+ if (context->status & MONO_RELATIONS_EVALUATION_IS_RECURSIVE) {
+ if (TRACE_ABC_REMOVAL) {
+ printf ("Recursivity detected for varible %d (target variable %d), status ", variable, target_variable);
+ print_evaluation_context_status (context->status);
+ }
+
+ // If we are, check if the evaluation of the related variable is complete
+ if (related_context->status == MONO_RELATIONS_EVALUATION_COMPLETED) {
+ // If it is complete, we are part of a recursive definition.
+ // Since it is a *definition* (and definitions are evaluated *before*
+ // conditions because they are first in the list), intersection is not
+ // strictly necessary, we simply copy the ranges and apply the delta
+ context->ranges = related_context->ranges;
+ /* Delta has already been checked for over/under-flow when evaluating values */
+ MONO_ADD_DELTA_SAFELY_TO_RANGES (context->ranges, relation->related_value.value.variable.delta);
+ context->status = MONO_RELATIONS_EVALUATION_COMPLETED;
+ if (TRACE_ABC_REMOVAL) {
+ printf (", ranges already computed, result: \n");
+ print_evaluation_context_ranges (&(context->ranges));
+ printf (" (delta is %d)\n", relation->related_value.value.variable.delta);
+ }
+ } else {
+ // If it is not complete, do nothing (we do not have enough information)
+ if (TRACE_ABC_REMOVAL) {
+ printf (", ranges not computed\n");
+ }
+ }
+ } else {
+ // If we are not (the common case) intersect the result
+ intersect_ranges( &(context->ranges), &(related_context->ranges), relation->related_value.value.variable.delta, relation->relation );
+ }
+ } else {
+ if (TRACE_ABC_REMOVAL) {
+ printf ("Relation is a back-edge in this traversal, skipping\n");
+ }
+ }
+ }
+ break;
+ case MONO_PHI_SUMMARIZED_VALUE: {
+ // We must compute all PHI alternatives, combining the results (with a union, which is a logical "or"),
+ // and intersect this result with the ranges in the context; we must also take into account recursions
+ // (with loops that can be ascending, descending, or indefinite)
+ MonoRelationsEvaluationRanges phi_ranges;