diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 0c6e361c05f..28c25464564 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -2142,13 +2142,17 @@ void goto_checkt::goto_check( { // These are further 'exit points' of the program const exprt simplified_guard = simplify_expr(i.guard, ns); + // The function may be inlined to only __CPROVER_start, use the + // original location (if it is still valid thanks to setting + // adjust_false=false in goto_inlinet). + const irep_idt &former_function = i.source_location.get_function(); if( enable_memory_cleanup_check && simplified_guard.is_false() && - (function_identifier == "abort" || function_identifier == "exit" || - function_identifier == "_Exit" || + (former_function == "abort" || former_function == "exit" || + former_function == "_Exit" || (i.labels.size() == 1 && i.labels.front() == "__VERIFIER_abort"))) { - memory_leak_check(function_identifier); + memory_leak_check(former_function); } if(!enable_assumptions) { diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index afd11c14754..08ff39dfaea 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -246,8 +246,10 @@ static bool filter_out( prev_it->pc->source_location==it->pc->source_location) return true; +#if 0 if(it->is_goto() && it->pc->get_condition().is_true()) return true; +#endif const source_locationt &source_location=it->pc->source_location; diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp index 1319015eafb..cff290e8d7e 100644 --- a/src/xmllang/graphml.cpp +++ b/src/xmllang/graphml.cpp @@ -390,16 +390,6 @@ bool write_graphml(const graphmlt &src, std::ostream &os) key.set_attribute("id", "architecture"); } - // - { - xmlt &key=graphml.new_element("key"); - key.set_attribute("attr.name", "creationTime"); - key.set_attribute("attr.type", "string"); - key.set_attribute("for", "graph"); - key.set_attribute("id", "creationtime"); - } - // {