real_absolute: turn this code on
[smatch.git] / smatch_implied.c
blobfec771bd8cda6f2cc9ab2dd56a7a3c77e955edcf
1 /*
2 * Copyright (C) 2008 Dan Carpenter.
4 * This program is free software; you can redistribute it and/or
5 * modify it under the terms of the GNU General Public License
6 * as published by the Free Software Foundation; either version 2
7 * of the License, or (at your option) any later version.
9 * This program is distributed in the hope that it will be useful,
10 * but WITHOUT ANY WARRANTY; without even the implied warranty of
11 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 * GNU General Public License for more details.
14 * You should have received a copy of the GNU General Public License
15 * along with this program; if not, see http://www.gnu.org/copyleft/gpl.txt
19 * Imagine we have this code:
20 * foo = 1;
21 * if (bar)
22 * foo = 99;
23 * else
24 * frob();
25 * // <-- point #1
26 * if (foo == 99) // <-- point #2
27 * bar->baz; // <-- point #3
30 * At point #3 bar is non null and can be dereferenced.
32 * It's smatch_implied.c which sets bar to non null at point #2.
34 * At point #1 merge_slist() stores the list of states from both
35 * the true and false paths. On the true path foo == 99 and on
36 * the false path foo == 1. merge_slist() sets their pool
37 * list to show the other states which were there when foo == 99.
39 * When it comes to the if (foo == 99) the smatch implied hook
40 * looks for all the pools where foo was not 99. It makes a list
41 * of those.
43 * Then for bar (and all the other states) it says, ok bar is a
44 * merged state that came from these previous states. We'll
45 * chop out all the states where it came from a pool where
46 * foo != 99 and merge it all back together.
48 * That is the implied state of bar.
50 * merge_slist() sets up ->pool. An sm_state only has one ->pool and
51 * that is the pool where it was first set. The my pool gets set when
52 * code paths merge. States that have been set since the last merge do
53 * not have a ->pool.
54 * merge_sm_state() sets ->left and ->right. (These are the states which were
55 * merged to form the current state.)
56 * a pool: a pool is an slist that has been merged with another slist.
59 #include <sys/time.h>
60 #include <time.h>
61 #include "smatch.h"
62 #include "smatch_slist.h"
63 #include "smatch_extra.h"
65 char *implied_debug_msg;
66 #define DIMPLIED(msg...) do { if (option_debug_implied) printf(msg); } while (0)
68 int option_debug_implied = 0;
71 * tmp_range_list():
72 * It messes things up to free range list allocations. This helper fuction
73 * lets us reuse memory instead of doing new allocations.
75 static struct range_list *tmp_range_list(struct symbol *type, long long num)
77 static struct range_list *my_list = NULL;
78 static struct data_range *my_range;
80 __free_ptr_list((struct ptr_list **)&my_list);
81 my_range = alloc_range(ll_to_sval(num), ll_to_sval(num));
82 add_ptr_list(&my_list, my_range);
83 return my_list;
86 static void print_debug_tf(struct sm_state *sm, int istrue, int isfalse)
88 if (!option_debug_implied && !option_debug)
89 return;
91 if (istrue && isfalse) {
92 printf("'%s = %s' from %d does not exist.\n", sm->name,
93 show_state(sm->state), sm->line);
94 } else if (istrue) {
95 printf("'%s = %s' from %d is true. [stree %d]\n", sm->name, show_state(sm->state),
96 sm->line, get_stree_id(sm->pool));
97 } else if (isfalse) {
98 printf("'%s = %s' from %d is false. [stree %d]\n", sm->name, show_state(sm->state),
99 sm->line, get_stree_id(sm->pool));
100 } else {
101 printf("'%s = %s' from %d could be true or false. [stree %d]\n", sm->name,
102 show_state(sm->state), sm->line, get_stree_id(sm->pool));
107 * add_pool() adds a slist to *pools. If the slist has already been
108 * added earlier then it doesn't get added a second time.
110 void add_pool(struct stree_stack **pools, struct stree *new)
112 struct stree *tmp;
114 FOR_EACH_PTR(*pools, tmp) {
115 if (tmp < new)
116 continue;
117 else if (tmp == new) {
118 return;
119 } else {
120 INSERT_CURRENT(new, tmp);
121 return;
123 } END_FOR_EACH_PTR(tmp);
124 add_ptr_list(pools, new);
128 * If 'foo' == 99 add it that pool to the true pools. If it's false, add it to
129 * the false pools. If we're not sure, then we don't add it to either.
131 static void do_compare(struct sm_state *sm, int comparison, struct range_list *rl,
132 struct stree_stack **true_stack,
133 struct stree_stack **false_stack)
135 struct sm_state *s;
136 int istrue;
137 int isfalse;
138 struct range_list *var_rl;
140 if (!sm->pool)
141 return;
143 if (is_implied(sm)) {
144 s = get_sm_state_stree(sm->pool,
145 sm->owner, sm->name,
146 sm->sym);
147 } else {
148 s = sm;
151 if (!s) {
152 if (option_debug_implied || option_debug)
153 sm_msg("%s from %d, has borrowed implications.",
154 sm->name, sm->line);
155 return;
158 var_rl = cast_rl(rl_type(rl), estate_rl(s->state));
160 istrue = !possibly_false_rl(var_rl, comparison, rl);
161 isfalse = !possibly_true_rl(var_rl, comparison, rl);
163 print_debug_tf(s, istrue, isfalse);
165 if (istrue)
166 add_pool(true_stack, s->pool);
168 if (isfalse)
169 add_pool(false_stack, s->pool);
172 static int pool_in_pools(struct stree *pool,
173 const struct stree_stack *pools)
175 struct stree *tmp;
177 FOR_EACH_PTR(pools, tmp) {
178 if (tmp == pool)
179 return 1;
180 if (tmp > pool)
181 return 0;
182 } END_FOR_EACH_PTR(tmp);
183 return 0;
186 static int is_checked(struct state_list *checked, struct sm_state *sm)
188 struct sm_state *tmp;
190 FOR_EACH_PTR(checked, tmp) {
191 if (tmp == sm)
192 return 1;
193 } END_FOR_EACH_PTR(tmp);
194 return 0;
198 * separate_pools():
199 * Example code: if (foo == 99) {
201 * Say 'foo' is a merged state that has many possible values. It is the combination
202 * of merges. separate_pools() iterates through the pools recursively and calls
203 * do_compare() for each time 'foo' was set.
205 static void separate_pools(struct sm_state *sm, int comparison, struct range_list *rl,
206 struct stree_stack **true_stack,
207 struct stree_stack **false_stack,
208 struct state_list **checked)
210 int free_checked = 0;
211 struct state_list *checked_states = NULL;
213 if (!sm)
214 return;
217 Sometimes the implications are just too big to deal with
218 so we bail. Theoretically, bailing out here can cause more false
219 positives but won't hide actual bugs.
221 if (sm->nr_children > 4000) {
222 if (option_debug || option_debug_implied) {
223 static char buf[1028];
224 snprintf(buf, sizeof(buf), "debug: separate_pools: nr_children over 4000 (%d). (%s %s)",
225 sm->nr_children, sm->name, show_state(sm->state));
226 implied_debug_msg = buf;
228 return;
231 if (checked == NULL) {
232 checked = &checked_states;
233 free_checked = 1;
235 if (is_checked(*checked, sm))
236 return;
237 add_ptr_list(checked, sm);
239 do_compare(sm, comparison, rl, true_stack, false_stack);
241 separate_pools(sm->left, comparison, rl, true_stack, false_stack, checked);
242 separate_pools(sm->right, comparison, rl, true_stack, false_stack, checked);
243 if (free_checked)
244 free_slist(checked);
247 struct sm_state *filter_pools(struct sm_state *sm,
248 const struct stree_stack *remove_stack,
249 const struct stree_stack *keep_stack,
250 int *modified)
252 struct sm_state *ret = NULL;
253 struct sm_state *left;
254 struct sm_state *right;
255 int removed = 0;
257 if (!sm)
258 return NULL;
260 if (sm->nr_children > 4000) {
261 if (option_debug || option_debug_implied) {
262 static char buf[1028];
263 snprintf(buf, sizeof(buf), "debug: %s: nr_children over 4000 (%d). (%s %s)",
264 __func__, sm->nr_children, sm->name, show_state(sm->state));
265 implied_debug_msg = buf;
267 return NULL;
270 if (pool_in_pools(sm->pool, remove_stack)) {
271 DIMPLIED("removed %s from %d [stree %d]\n", show_sm(sm), sm->line, get_stree_id(sm->pool));
272 *modified = 1;
273 return NULL;
276 if (!is_merged(sm) || pool_in_pools(sm->pool, keep_stack)) {
277 DIMPLIED("kept %s from %d [stree %d]\n", show_sm(sm), sm->line, get_stree_id(sm->pool));
278 return sm;
281 DIMPLIED("checking %s from %d (%d) [stree %d] left = %s [stree %d] right = %s [stree %d]\n",
282 show_sm(sm), sm->line, sm->nr_children, get_stree_id(sm->pool),
283 sm->left ? show_sm(sm->left) : "<none>", sm->left ? get_stree_id(sm->left->pool) : -1,
284 sm->right ? show_sm(sm->right) : "<none>", sm->right ? get_stree_id(sm->right->pool) : -1);
285 left = filter_pools(sm->left, remove_stack, keep_stack, &removed);
286 right = filter_pools(sm->right, remove_stack, keep_stack, &removed);
287 if (!removed) {
288 DIMPLIED("kept %s from %d [stree %d]\n", show_sm(sm), sm->line, get_stree_id(sm->pool));
289 return sm;
291 *modified = 1;
292 if (!left && !right) {
293 DIMPLIED("removed %s from %d <none> [stree %d]\n", show_sm(sm), sm->line, get_stree_id(sm->pool));
294 return NULL;
297 if (!left) {
298 ret = clone_sm(right);
299 ret->merged = 1;
300 ret->right = right;
301 ret->left = NULL;
302 ret->pool = sm->pool;
303 } else if (!right) {
304 ret = clone_sm(left);
305 ret->merged = 1;
306 ret->left = left;
307 ret->right = NULL;
308 ret->pool = sm->pool;
309 } else {
310 ret = merge_sm_states(left, right);
311 ret->pool = sm->pool;
313 ret->implied = 1;
314 DIMPLIED("partial %s => ", show_sm(sm));
315 DIMPLIED("%s from %d [stree %d]\n", show_sm(ret), sm->line, get_stree_id(sm->pool));
316 return ret;
319 static int highest_stree_id(struct sm_state *sm)
321 int left = 0;
322 int right = 0;
324 if (!sm->left && !sm->right)
325 return 0;
327 if (sm->left)
328 left = get_stree_id(sm->left->pool);
329 if (sm->right)
330 right = get_stree_id(sm->right->pool);
332 if (right > left)
333 return right;
334 return left;
337 static struct stree *filter_stack(struct sm_state *gate_sm,
338 struct stree *pre_stree,
339 const struct stree_stack *remove_stack,
340 const struct stree_stack *keep_stack)
342 struct stree *ret = NULL;
343 struct sm_state *tmp;
344 struct sm_state *filtered_sm;
345 int modified;
347 if (!remove_stack)
348 return NULL;
350 FOR_EACH_SM(pre_stree, tmp) {
351 if (!tmp->merged)
352 continue;
353 if (highest_stree_id(tmp) < highest_stree_id(gate_sm)) {
354 DIMPLIED("skipping %s. set before. %d vs %d\n",
355 tmp->name, highest_stree_id(tmp),
356 highest_stree_id(gate_sm));
357 continue;
359 modified = 0;
360 filtered_sm = filter_pools(tmp, remove_stack, keep_stack, &modified);
361 if (filtered_sm && modified) {
362 /* the assignments here are for borrowed implications */
363 filtered_sm->name = tmp->name;
364 filtered_sm->sym = tmp->sym;
365 avl_insert(&ret, filtered_sm);
366 if (out_of_memory())
367 return NULL;
370 } END_FOR_EACH_SM(tmp);
371 return ret;
374 static void separate_and_filter(struct sm_state *sm, int comparison, struct range_list *rl,
375 struct stree *pre_stree,
376 struct stree **true_states,
377 struct stree **false_states)
379 struct stree_stack *true_stack = NULL;
380 struct stree_stack *false_stack = NULL;
381 struct timeval time_before;
382 struct timeval time_after;
384 gettimeofday(&time_before, NULL);
386 if (!is_merged(sm)) {
387 DIMPLIED("%d '%s' is not merged.\n", get_lineno(), sm->name);
388 return;
391 if (option_debug_implied || option_debug) {
392 sm_msg("checking implications: (%s %s %s)",
393 sm->name, show_special(comparison), show_rl(rl));
396 separate_pools(sm, comparison, rl, &true_stack, &false_stack, NULL);
398 DIMPLIED("filtering true stack.\n");
399 *true_states = filter_stack(sm, pre_stree, false_stack, true_stack);
400 DIMPLIED("filtering false stack.\n");
401 *false_states = filter_stack(sm, pre_stree, true_stack, false_stack);
402 free_stree_stack(&true_stack);
403 free_stree_stack(&false_stack);
404 if (option_debug_implied || option_debug) {
405 printf("These are the implied states for the true path:\n");
406 __print_stree(*true_states);
407 printf("These are the implied states for the false path:\n");
408 __print_stree(*false_states);
411 gettimeofday(&time_after, NULL);
412 if (time_after.tv_sec - time_before.tv_sec > 7)
413 __bail_on_rest_of_function = 1;
416 static struct expression *get_left_most_expr(struct expression *expr)
418 expr = strip_expr(expr);
419 if (expr->type == EXPR_ASSIGNMENT)
420 return get_left_most_expr(expr->left);
421 return expr;
424 static int is_merged_expr(struct expression *expr)
426 struct sm_state *sm;
427 sval_t dummy;
429 if (get_value(expr, &dummy))
430 return 0;
431 sm = get_sm_state_expr(SMATCH_EXTRA, expr);
432 if (!sm)
433 return 0;
434 if (is_merged(sm))
435 return 1;
436 return 0;
439 static void delete_equiv_stree(struct stree **stree, const char *name, struct symbol *sym)
441 struct smatch_state *state;
442 struct relation *rel;
444 state = get_state(SMATCH_EXTRA, name, sym);
445 if (!estate_related(state)) {
446 delete_state_stree(stree, SMATCH_EXTRA, name, sym);
447 return;
450 FOR_EACH_PTR(estate_related(state), rel) {
451 delete_state_stree(stree, SMATCH_EXTRA, rel->name, rel->sym);
452 } END_FOR_EACH_PTR(rel);
455 static int handle_comparison(struct expression *expr,
456 struct stree **implied_true,
457 struct stree **implied_false)
459 struct sm_state *sm = NULL;
460 struct range_list *rl = NULL;
461 struct expression *left;
462 struct expression *right;
463 struct symbol *type;
464 int comparison = expr->op;
466 left = get_left_most_expr(expr->left);
467 right = get_left_most_expr(expr->right);
469 if (is_merged_expr(left)) {
470 sm = get_sm_state_expr(SMATCH_EXTRA, left);
471 get_implied_rl(right, &rl);
472 } else if (is_merged_expr(right)) {
473 sm = get_sm_state_expr(SMATCH_EXTRA, right);
474 get_implied_rl(left, &rl);
475 comparison = flip_comparison(comparison);
478 if (!rl || !sm) {
479 free_rl(&rl);
480 return 0;
483 type = estate_type(sm->state);
484 if (type_positive_bits(rl_type(rl)) > type_positive_bits(type))
485 type = rl_type(rl);
486 if (type_positive_bits(type) < 31)
487 type = &int_ctype;
488 rl = cast_rl(type, rl);
490 separate_and_filter(sm, comparison, rl, __get_cur_stree(), implied_true, implied_false);
491 free_rl(&rl);
492 delete_equiv_stree(implied_true, sm->name, sm->sym);
493 delete_equiv_stree(implied_false, sm->name, sm->sym);
495 return 1;
498 static int handle_zero_comparison(struct expression *expr,
499 struct stree **implied_true,
500 struct stree **implied_false)
502 struct symbol *sym;
503 char *name;
504 struct sm_state *sm;
505 int ret = 0;
507 if (expr->type == EXPR_POSTOP)
508 expr = strip_expr(expr->unop);
510 if (expr->type == EXPR_ASSIGNMENT) {
511 /* most of the time ->pools will be empty here because we
512 just set the state, but if have assigned a conditional
513 function there are implications. */
514 expr = expr->left;
517 name = expr_to_var_sym(expr, &sym);
518 if (!name || !sym)
519 goto free;
520 sm = get_sm_state(SMATCH_EXTRA, name, sym);
521 if (!sm)
522 goto free;
524 separate_and_filter(sm, SPECIAL_NOTEQUAL, tmp_range_list(estate_type(sm->state), 0), __get_cur_stree(), implied_true, implied_false);
525 delete_equiv_stree(implied_true, name, sym);
526 delete_equiv_stree(implied_false, name, sym);
527 ret = 1;
528 free:
529 free_string(name);
530 return ret;
533 static int handled_by_implied_hook(struct expression *expr,
534 struct stree **implied_true,
535 struct stree **implied_false)
537 struct stree_stack *true_stack = NULL;
538 struct stree_stack *false_stack = NULL;
539 struct stree *pre_stree;
540 struct sm_state *sm;
542 sm = comparison_implication_hook(expr, &true_stack, &false_stack);
543 if (!sm)
544 return 0;
546 pre_stree = clone_stree(__get_cur_stree());
548 *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
549 *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
551 free_stree(&pre_stree);
552 free_stree_stack(&true_stack);
553 free_stree_stack(&false_stack);
555 return 1;
558 static int handled_by_extra_states(struct expression *expr,
559 struct stree **implied_true,
560 struct stree **implied_false)
562 if (expr->type == EXPR_COMPARE)
563 return handle_comparison(expr, implied_true, implied_false);
564 else
565 return handle_zero_comparison(expr, implied_true, implied_false);
569 static int handled_by_stored_conditions(struct expression *expr,
570 struct stree **implied_true,
571 struct stree **implied_false)
573 struct stree_stack *true_stack = NULL;
574 struct stree_stack *false_stack = NULL;
575 struct stree *pre_stree;
576 struct sm_state *sm;
578 sm = stored_condition_implication_hook(expr, &true_stack, &false_stack);
579 if (!sm)
580 return 0;
582 pre_stree = clone_stree(__get_cur_stree());
584 *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
585 *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
587 free_stree(&pre_stree);
588 free_stree_stack(&true_stack);
589 free_stree_stack(&false_stack);
591 return 1;
594 static int found_implications;
595 static void get_tf_states(struct expression *expr,
596 struct stree **implied_true,
597 struct stree **implied_false)
599 if (handled_by_implied_hook(expr, implied_true, implied_false))
600 goto found;
602 if (handled_by_extra_states(expr, implied_true, implied_false))
603 goto found;
605 if (handled_by_stored_conditions(expr, implied_true, implied_false))
606 goto found;
608 return;
609 found:
610 found_implications = 1;
613 static struct stree *saved_implied_true;
614 static struct stree *saved_implied_false;
616 static void save_implications_hook(struct expression *expr)
618 get_tf_states(expr, &saved_implied_true, &saved_implied_false);
621 static void set_implied_states(struct expression *expr)
623 struct sm_state *sm;
625 FOR_EACH_SM(saved_implied_true, sm) {
626 __set_true_false_sm(sm, NULL);
627 } END_FOR_EACH_SM(sm);
628 free_stree(&saved_implied_true);
630 FOR_EACH_SM(saved_implied_false, sm) {
631 __set_true_false_sm(NULL, sm);
632 } END_FOR_EACH_SM(sm);
633 free_stree(&saved_implied_false);
636 void param_limit_implications(struct expression *expr, int param, char *key, char *value)
638 struct expression *arg;
639 struct symbol *compare_type;
640 char *name;
641 struct symbol *sym;
642 struct sm_state *sm;
643 struct sm_state *tmp;
644 struct stree *implied_true = NULL;
645 struct stree *implied_false = NULL;
646 struct range_list *orig, *limit, *rl;
648 while (expr->type == EXPR_ASSIGNMENT)
649 expr = strip_expr(expr->right);
650 if (expr->type != EXPR_CALL)
651 return;
653 arg = get_argument_from_call_expr(expr->args, param);
654 if (!arg)
655 return;
657 name = get_variable_from_key(arg, key, &sym);
658 if (!name || !sym)
659 goto free;
661 sm = get_sm_state(SMATCH_EXTRA, name, sym);
662 if (!sm || !sm->merged)
663 goto free;
665 if (strcmp(key, "$") == 0)
666 compare_type = get_arg_type(expr->fn, param);
667 else
668 compare_type = get_member_type_from_key(arg, key);
670 orig = estate_rl(sm->state);
671 orig = cast_rl(compare_type, orig);
673 call_results_to_rl(expr, compare_type, value, &limit);
674 rl = rl_intersection(orig, limit);
676 separate_and_filter(sm, SPECIAL_EQUAL, rl, __get_cur_stree(), &implied_true, &implied_false);
678 FOR_EACH_SM(implied_true, tmp) {
679 __set_sm_fake_stree(tmp);
680 } END_FOR_EACH_SM(tmp);
682 free_stree(&implied_true);
683 free_stree(&implied_false);
684 free:
685 free_string(name);
688 struct range_list *__get_implied_values(struct expression *switch_expr)
690 char *name;
691 struct symbol *sym;
692 struct smatch_state *state;
693 struct range_list *ret = NULL;
695 name = expr_to_var_sym(switch_expr, &sym);
696 if (!name || !sym)
697 goto free;
698 state = get_state(SMATCH_EXTRA, name, sym);
699 if (!state)
700 goto free;
701 ret = clone_rl(estate_rl(state));
702 free:
703 free_string(name);
704 if (!ret) {
705 struct symbol *type;
707 type = get_type(switch_expr);
708 ret = alloc_rl(sval_type_min(type), sval_type_max(type));
710 return ret;
713 struct stree *__implied_case_stree(struct expression *switch_expr,
714 struct expression *case_expr,
715 struct expression *case_to,
716 struct range_list_stack **remaining_cases,
717 struct stree **raw_stree)
719 char *name = NULL;
720 struct symbol *sym;
721 struct sm_state *sm;
722 struct stree *true_states = NULL;
723 struct stree *false_states = NULL;
724 struct stree *extra_states = NULL;
725 struct stree *ret = clone_stree(*raw_stree);
726 sval_t start, end;
727 struct range_list *rl = NULL;
729 name = expr_to_var_sym(switch_expr, &sym);
730 if (!name || !sym)
731 goto free;
732 sm = get_sm_state_stree(*raw_stree, SMATCH_EXTRA, name, sym);
734 if (get_value(case_to, &end) && get_value(case_expr, &start)) {
735 filter_top_rl(remaining_cases, start, end);
736 add_range(&rl, start, end);
737 } else if (get_value(case_expr, &start)) {
738 filter_top_rl(remaining_cases, start, start);
739 add_range(&rl, start, start);
740 } else {
741 rl = clone_rl(top_rl(*remaining_cases));
744 if (sm)
745 separate_and_filter(sm, SPECIAL_EQUAL, rl, *raw_stree, &true_states, &false_states);
747 __push_fake_cur_stree();
748 __unnullify_path();
749 set_extra_nomod(name, sym, alloc_estate_rl(rl));
750 extra_states = __pop_fake_cur_stree();
751 overwrite_stree(extra_states, &true_states);
752 overwrite_stree(true_states, &ret);
753 free_stree(&extra_states);
754 free_stree(&true_states);
755 free_stree(&false_states);
756 free:
757 free_string(name);
758 return ret;
761 static void match_end_func(struct symbol *sym)
763 if (__inline_fn)
764 return;
765 implied_debug_msg = NULL;
768 static int sm_state_in_slist(struct sm_state *sm, struct state_list *slist)
770 struct sm_state *tmp;
772 FOR_EACH_PTR(slist, tmp) {
773 if (tmp == sm)
774 return 1;
775 } END_FOR_EACH_PTR(tmp);
776 return 0;
780 * The situation is we have a SMATCH_EXTRA state and we want to break it into
781 * each of the ->possible states and find the implications of each. The caller
782 * has to use __push_fake_cur_stree() to preserve the correct states so they
783 * can be restored later.
785 void overwrite_states_using_pool(struct sm_state *sm)
787 struct sm_state *old;
788 struct sm_state *new;
790 if (!sm->pool)
791 return;
793 FOR_EACH_SM(sm->pool, old) {
794 new = get_sm_state(old->owner, old->name, old->sym);
795 if (!new) /* the variable went out of scope */
796 continue;
797 if (sm_state_in_slist(old, new->possible))
798 set_state(old->owner, old->name, old->sym, old->state);
799 } END_FOR_EACH_SM(old);
802 int assume(struct expression *expr)
804 int orig_final_pass = final_pass;
806 final_pass = 0;
807 __push_fake_cur_stree();
808 found_implications = 0;
809 __split_whole_condition(expr);
810 final_pass = orig_final_pass;
812 if (!found_implications) {
813 __discard_false_states();
814 __free_fake_cur_stree();
815 return 0;
818 return 1;
821 void end_assume(void)
823 __discard_false_states();
824 __free_fake_cur_stree();
827 void __extra_match_condition(struct expression *expr);
828 void __comparison_match_condition(struct expression *expr);
829 void __stored_condition(struct expression *expr);
830 void register_implications(int id)
832 add_hook(&save_implications_hook, CONDITION_HOOK);
833 add_hook(&set_implied_states, CONDITION_HOOK);
834 add_hook(&__extra_match_condition, CONDITION_HOOK);
835 add_hook(&__comparison_match_condition, CONDITION_HOOK);
836 add_hook(&__stored_condition, CONDITION_HOOK);
837 add_hook(&match_end_func, END_FUNC_HOOK);