GraphML witnesses: correctly set the scope of parameters
We would previously use the name of the calling function. Instead, parameter assignments require a special case. Regression test kindly provided by @JanSvejda. Fixes: #4418
This commit is contained in:
parent
700587729f
commit
51e0cd71bb
|
@ -43,7 +43,7 @@ main.c
|
|||
<edge source="[0-9\.]*" target="[0-9\.]*">
|
||||
<data key="originfile">main.c</data>
|
||||
<data key="startline">29</data>
|
||||
<data key="assumption.scope">main</data>
|
||||
<data key="assumption.scope">remove_one</data>
|
||||
</edge>
|
||||
<node id="[0-9\.]*"/>
|
||||
<edge source="[0-9\.]*" target="[0-9\.]*">
|
||||
|
|
|
@ -0,0 +1,31 @@
|
|||
extern void __VERIFIER_error();
|
||||
|
||||
static float one(float *foo)
|
||||
{
|
||||
return *foo;
|
||||
}
|
||||
|
||||
static float two(float *foo)
|
||||
{
|
||||
return *foo;
|
||||
}
|
||||
|
||||
float x = 0;
|
||||
|
||||
void step()
|
||||
{
|
||||
x = one(0);
|
||||
}
|
||||
|
||||
int main(void)
|
||||
{
|
||||
while(1)
|
||||
{
|
||||
step();
|
||||
if(x == 0)
|
||||
{
|
||||
__VERIFIER_error();
|
||||
}
|
||||
}
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,10 @@
|
|||
CORE
|
||||
main.c
|
||||
--graphml-witness - --unwindset main.0:1 --unwinding-assertions
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION FAILED$
|
||||
<data key="assumption">foo = \(\(float \*\)0\);</data>
|
||||
<data key="assumption.scope">one</data>
|
||||
--
|
||||
^warning: ignoring
|
|
@ -466,7 +466,13 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
|
|||
|
||||
xmlt &val_s = edge.new_element("data");
|
||||
val_s.set_attribute("key", "assumption.scope");
|
||||
val_s.data = id2string(it->function_id);
|
||||
irep_idt function_id = it->function_id;
|
||||
const symbolt *symbol_ptr = nullptr;
|
||||
if(!ns.lookup(lhs_id, symbol_ptr) && symbol_ptr->is_parameter)
|
||||
{
|
||||
function_id = lhs_id.substr(0, lhs_id.find("::"));
|
||||
}
|
||||
val_s.data = id2string(function_id);
|
||||
|
||||
if(has_prefix(val.data, "\\result ="))
|
||||
{
|
||||
|
|
Loading…
Reference in New Issue