From bce1feabb7db46a7ddeac01644959b3b95a550c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franti=C5=A1ek=20Ne=C4=8Das?= Date: Mon, 11 Oct 2021 07:54:38 +0200 Subject: [PATCH 1/3] Revert "Witnesses: add the 'creationtime' attribute" This reverts commit 40046b2c64e410b08900baaae92f4a3f014f194b. A commit achieving the same thing is already present in CBMC causing duplication of the attribute. --- src/xmllang/graphml.cpp | 10 ---------- 1 file changed, 10 deletions(-) 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"); - } - // { From 8f5c6ef61b9214caa5d7da42929c912e44b59392 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franti=C5=A1ek=20Ne=C4=8Das?= Date: Fri, 15 Oct 2021 12:52:56 +0200 Subject: [PATCH 2/3] Correctly consider inlining when searching abort MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit If inlining is performed, the function_identifier parameter will always be __CPROVER_start. However, the former function is still stored in the goto instruction and can be sued for the instrumentation Signed-off-by: František Nečas --- src/analyses/goto_check.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) 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) { From 36c8f773dd0428d2fbcd735fc10cd17cf1798d70 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franti=C5=A1ek=20Ne=C4=8Das?= Date: Sun, 24 Oct 2021 10:48:08 +0200 Subject: [PATCH 3/3] Do not ignore edges if cond is true MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This was previously commented out but was dropped in the rebase by accident (the code was moved and merge conflict not correctly resolved). This is necessary for some nontermination witnesses to function correctly. Signed-off-by: František Nečas --- src/goto-programs/graphml_witness.cpp | 2 ++ 1 file changed, 2 insertions(+) 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;