-
Notifications
You must be signed in to change notification settings - Fork 84
Closed
Description
In some cases recursive functions cause arg/lookup to return nodes that have edges to ARG nodes that don't exist.
Reproduction:
// recursion.c
int fib(int n) {
if (n < 2) {
return 1;
}
return fib(n - 1) + fib(n - 2);
}
int main() {
int a;
fib(a);
}// goblint.json
{
"files": ["recursion.c"]
}{"jsonrpc":"2.0","id":"20","method":"arg/lookup","params":{"node":"fun1620fib(18)[15]"}}returns
{"id":"20","jsonrpc":"2.0","result":[{"node":"fun1620fib(18)[15]","cfg_node":"fun1620","context":"18","path":"15","location":{"file":"recursion.c","line":1,"column":1,"byte":136,"endLine":6,"endColumn":1,"endByte":230},"function":"fib","next":[{"edge":{"cfg":{"string":"(body)","type":"entry","function":"fib"}},"node":"s77(18)[20]","cfg_node":"77","context":"18","path":"20","location":{"file":"recursion.c","line":2,"column":9,"byte":161,"endLine":2,"endColumn":14,"endByte":166},"function":"fib"}],"prev":[{"edge":{"entry":{"lval":null,"function":"fib","args":["a"]}},"node":"s84(9)[11]","cfg_node":"84","context":"9","path":"11","location":{"file":"recursion.c","line":10,"column":5,"byte":261,"endLine":10,"endColumn":11,"endByte":267},"function":"main"},{"edge":{"entry":{"lval":"tmp___0","function":"fib","args":["n - 2"]}},"node":"s81(18)[61]","cfg_node":"81","context":"18","path":"61","location":{"file":"recursion.c","line":5,"column":5,"byte":198,"endLine":5,"endColumn":35,"endByte":228},"function":"fib"},{"edge":{"entry":{"lval":"tmp___0","function":"fib","args":["n - 2"]}},"node":"s81(18)[38]","cfg_node":"81","context":"18","path":"38","location":{"file":"recursion.c","line":5,"column":5,"byte":198,"endLine":5,"endColumn":35,"endByte":228},"function":"fib"},{"edge":{"entry":{"lval":"tmp___0","function":"fib","args":["n - 2"]}},"node":"s81(18)[27]","cfg_node":"81","context":"18","path":"27","location":{"file":"recursion.c","line":5,"column":5,"byte":198,"endLine":5,"endColumn":35,"endByte":228},"function":"fib"},{"edge":{"entry":{"lval":"tmp","function":"fib","args":["n - 1"]}},"node":"s80(18)[27]","cfg_node":"80","context":"18","path":"27","location":{"file":"recursion.c","line":5,"column":5,"byte":198,"endLine":5,"endColumn":35,"endByte":228},"function":"fib"}]}]}Where the node s81(18)[61] does not exist according to both arg/lookup and arg/dot.
The issue seems to occur when analyzing with reset=true as well as reset=false.
Tested on Goblint version heads/master-0-g9daa89f52.