| 633 | } |
| 634 | |
| 635 | void |
| 636 | FactMgr::remove_loop_local_facts(const Statement* s, FactVec& facts) |
| 637 | { |
| 638 | // filter out out-of-scope facts |
| 639 | const Block* b = (s->eType==eBlock) ? (const Block*)s : s->parent; |
| 640 | vector<Variable*> local_vars = b->local_vars; |
| 641 | while (b && !b->looping) { |
| 642 | b = b->parent; |
| 643 | local_vars.insert(local_vars.end(), b->local_vars.begin(), b->local_vars.end()); |
| 644 | } |
| 645 | FactMgr::update_facts_for_oos_vars(local_vars, facts); |
| 646 | } |
| 647 | |
| 648 | void |
| 649 | FactMgr::output_assertions(std::ostream &out, const Statement* stm, int indent, bool post_condition) |