Print this page
12166 resync smatch to 0.6.1-rc1-il-3
*** 30,40 ****
#include "smatch.h"
#include "smatch_extra.h"
#include "smatch_slist.h"
! static int compare_id;
static int link_id;
static int inc_dec_id;
static int inc_dec_link_id;
static void add_comparison(struct expression *left, int comparison, struct expression *right);
--- 30,40 ----
#include "smatch.h"
#include "smatch_extra.h"
#include "smatch_slist.h"
! int comparison_id;
static int link_id;
static int inc_dec_id;
static int inc_dec_link_id;
static void add_comparison(struct expression *left, int comparison, struct expression *right);
*** 540,549 ****
--- 540,550 ----
{
struct compare_data *data = cur->state->data;
int extra, new;
static bool in_recurse;
+ // FIXME. No data is useless
if (!data)
return;
if (in_recurse)
return;
*** 554,564 ****
return;
new = comparison_intersection(extra, data->comparison);
if (new == data->comparison)
return;
! set_state(compare_id, cur->name, NULL,
alloc_compare_state(data->left, data->left_var, data->left_vsl,
new,
data->right, data->right_var, data->right_vsl));
}
--- 555,566 ----
return;
new = comparison_intersection(extra, data->comparison);
if (new == data->comparison)
return;
! // FIXME: we should always preserve implications
! set_state(comparison_id, cur->name, NULL,
alloc_compare_state(data->left, data->left_var, data->left_vsl,
new,
data->right, data->right_var, data->right_vsl));
}
*** 622,632 ****
add_var_sym(&right_vsl, orig, param);
state = alloc_compare_state(
NULL, param->ident->name, left_vsl,
SPECIAL_EQUAL,
NULL, alloc_sname(orig), right_vsl);
! set_state(compare_id, state_name, NULL, state);
link = alloc_sname(state_name);
links = NULL;
insert_string(&links, link);
state = alloc_link_state(links);
--- 624,634 ----
add_var_sym(&right_vsl, orig, param);
state = alloc_compare_state(
NULL, param->ident->name, left_vsl,
SPECIAL_EQUAL,
NULL, alloc_sname(orig), right_vsl);
! set_state(comparison_id, state_name, NULL, state);
link = alloc_sname(state_name);
links = NULL;
insert_string(&links, link);
state = alloc_link_state(links);
*** 673,683 ****
int op;
links = sm->state->data;
FOR_EACH_PTR(links, tmp) {
! state = get_state(compare_id, tmp, NULL);
if (!state)
continue;
data = state->data;
if (!data)
continue;
--- 675,685 ----
int op;
links = sm->state->data;
FOR_EACH_PTR(links, tmp) {
! state = get_state(comparison_id, tmp, NULL);
if (!state)
continue;
data = state->data;
if (!data)
continue;
*** 699,724 ****
break;
new = alloc_compare_state(
data->left, data->left_var, data->left_vsl,
flip ? '<' : '>',
data->right, data->right_var, data->right_vsl);
! set_state(compare_id, tmp, NULL, new);
break;
case '<':
case SPECIAL_UNSIGNED_LT:
new = alloc_compare_state(
data->left, data->left_var, data->left_vsl,
flip ? SPECIAL_GTE : SPECIAL_LTE,
data->right, data->right_var, data->right_vsl);
! set_state(compare_id, tmp, NULL, new);
break;
default:
new = alloc_compare_state(
data->left, data->left_var, data->left_vsl,
UNKNOWN_COMPARISON,
data->right, data->right_var, data->right_vsl);
! set_state(compare_id, tmp, NULL, new);
}
} END_FOR_EACH_PTR(tmp);
}
static void match_dec(struct sm_state *sm, bool preserve)
--- 701,726 ----
break;
new = alloc_compare_state(
data->left, data->left_var, data->left_vsl,
flip ? '<' : '>',
data->right, data->right_var, data->right_vsl);
! set_state(comparison_id, tmp, NULL, new);
break;
case '<':
case SPECIAL_UNSIGNED_LT:
new = alloc_compare_state(
data->left, data->left_var, data->left_vsl,
flip ? SPECIAL_GTE : SPECIAL_LTE,
data->right, data->right_var, data->right_vsl);
! set_state(comparison_id, tmp, NULL, new);
break;
default:
new = alloc_compare_state(
data->left, data->left_var, data->left_vsl,
UNKNOWN_COMPARISON,
data->right, data->right_var, data->right_vsl);
! set_state(comparison_id, tmp, NULL, new);
}
} END_FOR_EACH_PTR(tmp);
}
static void match_dec(struct sm_state *sm, bool preserve)
*** 731,741 ****
FOR_EACH_PTR(links, tmp) {
struct compare_data *data;
struct smatch_state *new;
! state = get_state(compare_id, tmp, NULL);
if (!state || !state->data)
continue;
data = state->data;
--- 733,743 ----
FOR_EACH_PTR(links, tmp) {
struct compare_data *data;
struct smatch_state *new;
! state = get_state(comparison_id, tmp, NULL);
if (!state || !state->data)
continue;
data = state->data;
*** 750,768 ****
new = alloc_compare_state(
data->left, data->left_var, data->left_vsl,
'<',
data->right, data->right_var, data->right_vsl);
! set_state(compare_id, tmp, NULL, new);
break;
}
default:
new = alloc_compare_state(
data->left, data->left_var, data->left_vsl,
UNKNOWN_COMPARISON,
data->right, data->right_var, data->right_vsl);
! set_state(compare_id, tmp, NULL, new);
}
} END_FOR_EACH_PTR(tmp);
}
static void reset_sm(struct sm_state *sm)
--- 752,770 ----
new = alloc_compare_state(
data->left, data->left_var, data->left_vsl,
'<',
data->right, data->right_var, data->right_vsl);
! set_state(comparison_id, tmp, NULL, new);
break;
}
default:
new = alloc_compare_state(
data->left, data->left_var, data->left_vsl,
UNKNOWN_COMPARISON,
data->right, data->right_var, data->right_vsl);
! set_state(comparison_id, tmp, NULL, new);
}
} END_FOR_EACH_PTR(tmp);
}
static void reset_sm(struct sm_state *sm)
*** 773,783 ****
links = sm->state->data;
FOR_EACH_PTR(links, tmp) {
struct smatch_state *old, *new;
! old = get_state(compare_id, tmp, NULL);
if (!old || !old->data) {
new = &undefined;
} else {
struct compare_data *data = old->data;
--- 775,785 ----
links = sm->state->data;
FOR_EACH_PTR(links, tmp) {
struct smatch_state *old, *new;
! old = get_state(comparison_id, tmp, NULL);
if (!old || !old->data) {
new = &undefined;
} else {
struct compare_data *data = old->data;
*** 784,794 ****
new = alloc_compare_state(
data->left, data->left_var, data->left_vsl,
UNKNOWN_COMPARISON,
data->right, data->right_var, data->right_vsl);
}
! set_state(compare_id, tmp, NULL, new);
} END_FOR_EACH_PTR(tmp);
set_state(link_id, sm->name, sm->sym, &undefined);
}
static bool match_add_sub_assign(struct sm_state *sm, struct expression *expr)
--- 786,796 ----
new = alloc_compare_state(
data->left, data->left_var, data->left_vsl,
UNKNOWN_COMPARISON,
data->right, data->right_var, data->right_vsl);
}
! set_state(comparison_id, tmp, NULL, new);
} END_FOR_EACH_PTR(tmp);
set_state(link_id, sm->name, sm->sym, &undefined);
}
static bool match_add_sub_assign(struct sm_state *sm, struct expression *expr)
*** 986,996 ****
right = left;
left = tmp;
}
snprintf(state_name, sizeof(state_name), "%s vs %s", left, right);
! state = get_state_stree(pre_stree, compare_id, state_name, NULL);
if (!state || !state->data)
return 0;
data = state->data;
if (flip)
return flip_comparison(data->comparison);
--- 988,998 ----
right = left;
left = tmp;
}
snprintf(state_name, sizeof(state_name), "%s vs %s", left, right);
! state = get_state_stree(pre_stree, comparison_id, state_name, NULL);
if (!state || !state->data)
return 0;
data = state->data;
if (flip)
return flip_comparison(data->comparison);
*** 1039,1049 ****
char *tmp;
char state_name[256];
struct var_sym *vs;
FOR_EACH_PTR(links, tmp) {
! state = get_state_stree(pre_stree, compare_id, tmp, NULL);
if (!state || !state->data)
continue;
data = state->data;
right_comparison = data->comparison;
right_expr = data->right;
--- 1041,1051 ----
char *tmp;
char state_name[256];
struct var_sym *vs;
FOR_EACH_PTR(links, tmp) {
! state = get_state_stree(pre_stree, comparison_id, tmp, NULL);
if (!state || !state->data)
continue;
data = state->data;
right_comparison = data->comparison;
right_expr = data->right;
*** 1098,1108 ****
right_expr, right_var, right_vsl);
else
false_state = NULL;
snprintf(state_name, sizeof(state_name), "%s vs %s", left_var, right_var);
! set_true_false_states(compare_id, state_name, NULL, true_state, false_state);
FOR_EACH_PTR(left_vsl, vs) {
save_link_var_sym(vs->var, vs->sym, state_name);
} END_FOR_EACH_PTR(vs);
FOR_EACH_PTR(right_vsl, vs) {
save_link_var_sym(vs->var, vs->sym, state_name);
--- 1100,1110 ----
right_expr, right_var, right_vsl);
else
false_state = NULL;
snprintf(state_name, sizeof(state_name), "%s vs %s", left_var, right_var);
! set_true_false_states(comparison_id, state_name, NULL, true_state, false_state);
FOR_EACH_PTR(left_vsl, vs) {
save_link_var_sym(vs->var, vs->sym, state_name);
} END_FOR_EACH_PTR(vs);
FOR_EACH_PTR(right_vsl, vs) {
save_link_var_sym(vs->var, vs->sym, state_name);
*** 1197,1207 ****
false_state = alloc_compare_state(
data->left, data->left_var, data->left_vsl,
SPECIAL_EQUAL,
data->right, data->right_var, data->right_vsl);
! set_true_false_states(compare_id, state_name, NULL, NULL, false_state);
}
static int is_plus_one(struct expression *expr)
{
sval_t sval;
--- 1199,1210 ----
false_state = alloc_compare_state(
data->left, data->left_var, data->left_vsl,
SPECIAL_EQUAL,
data->right, data->right_var, data->right_vsl);
! // FIXME: This doesn't handle links correct so it doesn't set "param orig"
! set_true_false_states(comparison_id, state_name, NULL, NULL, false_state);
}
static int is_plus_one(struct expression *expr)
{
sval_t sval;
*** 1338,1348 ****
pre_stree = clone_stree(__get_cur_stree());
update_tf_data(pre_stree, left_expr, left, left_vsl, right_expr, right, right_vsl, op, false_op);
free_stree(&pre_stree);
! set_true_false_states(compare_id, state_name, NULL, true_state, false_state);
__compare_param_limit_hook(left_expr, right_expr, state_name, true_state, false_state);
save_link(left_expr, state_name);
save_link(right_expr, state_name);
if (_false_state)
--- 1341,1351 ----
pre_stree = clone_stree(__get_cur_stree());
update_tf_data(pre_stree, left_expr, left, left_vsl, right_expr, right, right_vsl, op, false_op);
free_stree(&pre_stree);
! set_true_false_states(comparison_id, state_name, NULL, true_state, false_state);
__compare_param_limit_hook(left_expr, right_expr, state_name, true_state, false_state);
save_link(left_expr, state_name);
save_link(right_expr, state_name);
if (_false_state)
*** 1440,1450 ****
state = alloc_compare_state(
left_expr, left_name, left_vsl,
comparison,
right_expr, right_name, right_vsl);
! set_state(compare_id, state_name, NULL, state);
FOR_EACH_PTR(left_vsl, vs) {
save_link_var_sym(vs->var, vs->sym, state_name);
} END_FOR_EACH_PTR(vs);
FOR_EACH_PTR(right_vsl, vs) {
--- 1443,1453 ----
state = alloc_compare_state(
left_expr, left_name, left_vsl,
comparison,
right_expr, right_name, right_vsl);
! set_state(comparison_id, state_name, NULL, state);
FOR_EACH_PTR(left_vsl, vs) {
save_link_var_sym(vs->var, vs->sym, state_name);
} END_FOR_EACH_PTR(vs);
FOR_EACH_PTR(right_vsl, vs) {
*** 1490,1500 ****
state = alloc_compare_state(
left, left_name, left_vsl,
comparison,
right, right_name, right_vsl);
! set_state(compare_id, state_name, NULL, state);
save_link(left, state_name);
save_link(right, state_name);
free:
free_string(left_name);
--- 1493,1503 ----
state = alloc_compare_state(
left, left_name, left_vsl,
comparison,
right, right_name, right_vsl);
! set_state(comparison_id, state_name, NULL, state);
save_link(left, state_name);
save_link(right, state_name);
free:
free_string(left_name);
*** 1607,1617 ****
if (!state)
return;
links = state->data;
FOR_EACH_PTR(links, tmp) {
! state = get_state(compare_id, tmp, NULL);
if (!state || !state->data)
continue;
data = state->data;
comparison = data->comparison;
expr = data->right;
--- 1610,1620 ----
if (!state)
return;
links = state->data;
FOR_EACH_PTR(links, tmp) {
! state = get_state(comparison_id, tmp, NULL);
if (!state || !state->data)
continue;
data = state->data;
comparison = data->comparison;
expr = data->right;
*** 1676,1686 ****
two = tmp;
invert = 1;
}
snprintf(buf, sizeof(buf), "%s vs %s", one, two);
! state = get_state(compare_id, buf, NULL);
if (state)
ret = state_to_comparison(state);
if (invert)
ret = flip_comparison(ret);
--- 1679,1689 ----
two = tmp;
invert = 1;
}
snprintf(buf, sizeof(buf), "%s vs %s", one, two);
! state = get_state(comparison_id, buf, NULL);
if (state)
ret = state_to_comparison(state);
if (invert)
ret = flip_comparison(ret);
*** 1782,1792 ****
two = tmp;
comparison = flip_comparison(comparison);
}
snprintf(buf, sizeof(buf), "%s vs %s", one, two);
! sm = get_sm_state(compare_id, buf, NULL);
if (!sm)
goto free;
FOR_EACH_PTR(sm->possible, sm) {
if (!sm->state->data)
--- 1785,1795 ----
two = tmp;
comparison = flip_comparison(comparison);
}
snprintf(buf, sizeof(buf), "%s vs %s", one, two);
! sm = get_sm_state(comparison_id, buf, NULL);
if (!sm)
goto free;
FOR_EACH_PTR(sm->possible, sm) {
if (!sm->state->data)
*** 1823,1833 ****
if (!state)
return NULL;
links = state->data;
FOR_EACH_PTR(links, tmp) {
! sm = get_sm_state(compare_id, tmp, NULL);
if (!sm)
continue;
// FIXME have to compare name with vsl
add_ptr_list(&ret, sm);
} END_FOR_EACH_PTR(tmp);
--- 1826,1836 ----
if (!state)
return NULL;
links = state->data;
FOR_EACH_PTR(links, tmp) {
! sm = get_sm_state(comparison_id, tmp, NULL);
if (!sm)
continue;
// FIXME have to compare name with vsl
add_ptr_list(&ret, sm);
} END_FOR_EACH_PTR(tmp);
*** 1847,1857 ****
if (!state)
return NULL;
links = state->data;
FOR_EACH_PTR(links, tmp) {
! sm = get_sm_state(compare_id, tmp, NULL);
if (!sm)
continue;
if (!strchr(sm->state->name, '='))
continue;
if (strcmp(sm->state->name, "!=") == 0)
--- 1850,1860 ----
if (!state)
return NULL;
links = state->data;
FOR_EACH_PTR(links, tmp) {
! sm = get_sm_state(comparison_id, tmp, NULL);
if (!sm)
continue;
if (!strchr(sm->state->name, '='))
continue;
if (strcmp(sm->state->name, "!=") == 0)
*** 1877,1887 ****
if (!state)
return NULL;
links = state->data;
FOR_EACH_PTR(links, link) {
! sm = get_sm_state(compare_id, link, NULL);
if (!sm)
continue;
FOR_EACH_PTR(sm->possible, possible) {
if (strcmp(possible->state->name, "!=") != 0)
continue;
--- 1880,1890 ----
if (!state)
return NULL;
links = state->data;
FOR_EACH_PTR(links, link) {
! sm = get_sm_state(comparison_id, link, NULL);
if (!sm)
continue;
FOR_EACH_PTR(sm->possible, possible) {
if (strcmp(possible->state->name, "!=") != 0)
continue;
*** 1922,1932 ****
if (!state)
return;
links = state->data;
FOR_EACH_PTR(links, tmp) {
! state = get_state(compare_id, tmp, NULL);
if (!state || !state->data)
continue;
data = state->data;
comparison = data->comparison;
expr = data->right;
--- 1925,1935 ----
if (!state)
return;
links = state->data;
FOR_EACH_PTR(links, tmp) {
! state = get_state(comparison_id, tmp, NULL);
if (!state || !state->data)
continue;
data = state->data;
comparison = data->comparison;
expr = data->right;
*** 2171,2181 ****
struct var_sym *right_vs;
if (strstr(link, " orig"))
continue;
! sm = get_sm_state(compare_id, link, NULL);
if (!sm)
continue;
data = sm->state->data;
if (!data ||
data->comparison == UNKNOWN_COMPARISON ||
--- 2174,2184 ----
struct var_sym *right_vs;
if (strstr(link, " orig"))
continue;
! sm = get_sm_state(comparison_id, link, NULL);
if (!sm)
continue;
data = sm->state->data;
if (!data ||
data->comparison == UNKNOWN_COMPARISON ||
*** 2226,2236 ****
if (strstr(printed_name, " orig"))
return;
links = link_sm->state->data;
FOR_EACH_PTR(links, link) {
! compare_sm = get_sm_state(compare_id, link, NULL);
if (!compare_sm)
continue;
data = compare_sm->state->data;
if (!data || !data->comparison)
continue;
--- 2229,2239 ----
if (strstr(printed_name, " orig"))
return;
links = link_sm->state->data;
FOR_EACH_PTR(links, link) {
! compare_sm = get_sm_state(comparison_id, link, NULL);
if (!compare_sm)
continue;
data = compare_sm->state->data;
if (!data || !data->comparison)
continue;
*** 2319,2329 ****
FOR_EACH_MY_SM(link_id, __get_cur_stree(), tmp) {
if (get_param_num_from_sym(tmp->sym) < 0)
continue;
links = tmp->state->data;
FOR_EACH_PTR(links, link) {
! sm = get_sm_state(compare_id, link, NULL);
if (!sm)
continue;
data = sm->state->data;
if (!data ||
data->comparison == UNKNOWN_COMPARISON ||
--- 2322,2332 ----
FOR_EACH_MY_SM(link_id, __get_cur_stree(), tmp) {
if (get_param_num_from_sym(tmp->sym) < 0)
continue;
links = tmp->state->data;
FOR_EACH_PTR(links, link) {
! sm = get_sm_state(comparison_id, link, NULL);
if (!sm)
continue;
data = sm->state->data;
if (!data ||
data->comparison == UNKNOWN_COMPARISON ||
*** 2537,2547 ****
right_name = get_variable_from_key(right_arg, right_key, &right_sym);
if (!left_name || !right_name)
goto free;
snprintf(buf, sizeof(buf), "%s vs %s", left_name, right_name);
! state = get_state(compare_id, buf, NULL);
if (!state)
goto free;
state_op = state_to_comparison(state);
if (!state_op)
goto free;
--- 2540,2550 ----
right_name = get_variable_from_key(right_arg, right_key, &right_sym);
if (!left_name || !right_name)
goto free;
snprintf(buf, sizeof(buf), "%s vs %s", left_name, right_name);
! state = get_state(comparison_id, buf, NULL);
if (!state)
goto free;
state_op = state_to_comparison(state);
if (!state_op)
goto free;
*** 2571,2581 ****
return 0;
}
links = link_state->data;
FOR_EACH_PTR(links, link) {
! sm = get_sm_state(compare_id, link, NULL);
if (!sm)
continue;
data = sm->state->data;
if (!data)
continue;
--- 2574,2584 ----
return 0;
}
links = link_state->data;
FOR_EACH_PTR(links, link) {
! sm = get_sm_state(comparison_id, link, NULL);
if (!sm)
continue;
data = sm->state->data;
if (!data)
continue;
*** 2593,2608 ****
clear_compare_data_alloc();
}
void register_comparison(int id)
{
! compare_id = id;
! set_dynamic_states(compare_id);
add_hook(&save_start_states, AFTER_DEF_HOOK);
! add_unmatched_state_hook(compare_id, unmatched_comparison);
! add_pre_merge_hook(compare_id, &pre_merge_hook);
! add_merge_hook(compare_id, &merge_compare_states);
add_hook(&free_data, AFTER_FUNC_HOOK);
add_hook(&match_call_info, FUNCTION_CALL_HOOK);
add_split_return_callback(&print_return_comparison);
select_return_states_hook(PARAM_COMPARE, &db_return_comparison);
--- 2596,2611 ----
clear_compare_data_alloc();
}
void register_comparison(int id)
{
! comparison_id = id;
! set_dynamic_states(comparison_id);
add_hook(&save_start_states, AFTER_DEF_HOOK);
! add_unmatched_state_hook(comparison_id, unmatched_comparison);
! add_pre_merge_hook(comparison_id, &pre_merge_hook);
! add_merge_hook(comparison_id, &merge_compare_states);
add_hook(&free_data, AFTER_FUNC_HOOK);
add_hook(&match_call_info, FUNCTION_CALL_HOOK);
add_split_return_callback(&print_return_comparison);
select_return_states_hook(PARAM_COMPARE, &db_return_comparison);
*** 2637,2658 ****
inc_dec_link_id = id;
set_dynamic_states(inc_dec_link_id);
set_up_link_functions(inc_dec_id, inc_dec_link_id);
}
! static void filter_by_sm(struct sm_state *sm, int op,
struct state_list **true_stack,
struct state_list **false_stack)
{
struct compare_data *data;
int is_true = 0;
int is_false = 0;
if (!sm)
return;
data = sm->state->data;
! if (!data || data->comparison == UNKNOWN_COMPARISON)
goto split;
if (data->comparison == IMPOSSIBLE_COMPARISON)
return;
/*
--- 2640,2712 ----
inc_dec_link_id = id;
set_dynamic_states(inc_dec_link_id);
set_up_link_functions(inc_dec_id, inc_dec_link_id);
}
! static struct sm_state *clone_partial_sm(struct sm_state *sm, int comparison)
! {
! struct compare_data *data;
! struct sm_state *clone;
! struct stree *stree;
!
! data = sm->state->data;
!
! clone = clone_sm(sm);
! clone->state = alloc_compare_state(data->left, data->left_var, data->left_vsl,
! comparison,
! data->right, data->right_var, data->right_vsl);
! free_slist(&clone->possible);
! add_possible_sm(clone, clone);
!
! stree = clone_stree(sm->pool);
! overwrite_sm_state_stree(&stree, clone);
! clone->pool = stree;
!
! return clone;
! }
!
! static void create_fake_history(struct sm_state *sm, int op,
struct state_list **true_stack,
struct state_list **false_stack)
{
+ struct sm_state *true_sm, *false_sm;
struct compare_data *data;
+ int true_comparison;
+ int false_comparison;
+
+ data = sm->state->data;
+
+ if (is_merged(sm) || sm->left || sm->right)
+ return;
+
+ true_comparison = comparison_intersection(data->comparison, op);
+ false_comparison = comparison_intersection(data->comparison, negate_comparison(op));
+
+ true_sm = clone_partial_sm(sm, true_comparison);
+ false_sm = clone_partial_sm(sm, false_comparison);
+
+ sm->merged = 1;
+ sm->left = true_sm;
+ sm->right = false_sm;
+
+ add_ptr_list(true_stack, true_sm);
+ add_ptr_list(false_stack, false_sm);
+ }
+
+ static void filter_by_sm(struct sm_state *sm, int op,
+ struct state_list **true_stack,
+ struct state_list **false_stack,
+ bool *useful)
+ {
+ struct compare_data *data;
int is_true = 0;
int is_false = 0;
if (!sm)
return;
data = sm->state->data;
! if (!data)
goto split;
if (data->comparison == IMPOSSIBLE_COMPARISON)
return;
/*
*** 2665,2674 ****
--- 2719,2733 ----
if (data->comparison == comparison_intersection(data->comparison, op))
is_true = 1;
if (data->comparison == comparison_intersection(data->comparison, negate_comparison(op)))
is_false = 1;
+ if (!is_true && !is_false && !is_merged(sm)) {
+ create_fake_history(sm, op, true_stack, false_stack);
+ return;
+ }
+
if (debug_implied()) {
sm_msg("%s: %s: op = '%s' negated '%s'. true_intersect = '%s' false_insersect = '%s' sm = '%s'",
__func__,
sm->state->name,
alloc_sname(show_comparison(op)),
*** 2676,2692 ****
alloc_sname(show_comparison(comparison_intersection(data->comparison, op))),
alloc_sname(show_comparison(comparison_intersection(data->comparison, negate_comparison(op)))),
show_sm(sm));
}
if (is_true)
add_ptr_list(true_stack, sm);
if (is_false)
add_ptr_list(false_stack, sm);
split:
! filter_by_sm(sm->left, op, true_stack, false_stack);
! filter_by_sm(sm->right, op, true_stack, false_stack);
}
struct sm_state *comparison_implication_hook(struct expression *expr,
struct state_list **true_stack,
struct state_list **false_stack)
--- 2735,2752 ----
alloc_sname(show_comparison(comparison_intersection(data->comparison, op))),
alloc_sname(show_comparison(comparison_intersection(data->comparison, negate_comparison(op)))),
show_sm(sm));
}
+ *useful = true;
if (is_true)
add_ptr_list(true_stack, sm);
if (is_false)
add_ptr_list(false_stack, sm);
split:
! filter_by_sm(sm->left, op, true_stack, false_stack, useful);
! filter_by_sm(sm->right, op, true_stack, false_stack, useful);
}
struct sm_state *comparison_implication_hook(struct expression *expr,
struct state_list **true_stack,
struct state_list **false_stack)
*** 2693,2702 ****
--- 2753,2763 ----
{
struct sm_state *sm;
char *left, *right;
int op;
static char buf[256];
+ bool useful = false;
if (expr->type != EXPR_COMPARE)
return NULL;
op = expr->op;
*** 2716,2733 ****
right = tmp;
op = flip_comparison(op);
}
snprintf(buf, sizeof(buf), "%s vs %s", left, right);
! sm = get_sm_state(compare_id, buf, NULL);
if (!sm)
return NULL;
if (!sm->merged)
return NULL;
! filter_by_sm(sm, op, true_stack, false_stack);
! if (!*true_stack && !*false_stack)
return NULL;
if (debug_implied())
sm_msg("implications from comparison: (%s)", show_sm(sm));
--- 2777,2794 ----
right = tmp;
op = flip_comparison(op);
}
snprintf(buf, sizeof(buf), "%s vs %s", left, right);
! sm = get_sm_state(comparison_id, buf, NULL);
if (!sm)
return NULL;
if (!sm->merged)
return NULL;
! filter_by_sm(sm, op, true_stack, false_stack, &useful);
! if (!useful)
return NULL;
if (debug_implied())
sm_msg("implications from comparison: (%s)", show_sm(sm));