Clarification needed for line number information of returnFromFunction

[shaobo-he]

Hello sv-witnesses developers,

I have a quick question about combining startline with returnFromFunction. Specifically, I have two cases that I would need some clarification on.

1. Functions with explicit return statements
   In this case, I assume the startline should be the line of the return statement that the control flow exercises.

2. Functions without explicit return statements
   Consider the following example,

1 void myprint() {
2     if (0)
3       printf("hello, world\n");
4 }

What the startline of returnFromFunction would be?

Thanks,
Shaobo

[MartinSpiessl]

In CPAchecker we seem to simply notproduce a returnFromFunction transition if there is no return statement.
EDIT 2021-07-05: I think I was incorrect and we indeed do!

• program: returnfct.txt
• command line: scripts/cpa.sh -svcomp21 returnfct.c -spec config/properties/unreach-call.prp -timelimit 900s
• witness: witness.graphml.zip

Please note that for a witness you don't have to explicitly encode every call and return. There is always only one way I can exit a function without following any of the return statements inside, so the validator should be able to figure out that you left the function on its own.

Maybe for other validators that is different (@danieldietsch?), I would recommend to have a look at the witnesses and validation results of previous SV-COMPs, or just playing around with the validators to see what they accept.

[danieldietsch]

We print a returnFromFunction whenever our ICFG changes from one function to another, so we are not interested in the actual return statement.

During validation, we completely ignore this tag. Actually, while reviewing the code, I realised we still use the (very old) returnFrom key. So I assume CPAChecker does not use it as well?

[MartinSpiessl]

So I assume CPAChecker does not use it as well?

Do you mean the returnFrom? We use the returnFromFunction as far as I can tell. We don't use returnFrom, and I would expect that this will be rejected by the linter now since it is not mentioned in the format spec.

But looking at one of Ultimate's witnesses I think you are fine, you just rename the id of that key, but the attr.name is correct:

<key attr.name="returnFromFunction" attr.type="string" for="edge" id="returnFrom"/>

Still this should probably be checked against the linter.

Oh you probably mean whether we don't use the return statement? Yeah you are right, we don't mind if it is missing as well.

[MartinSpiessl]

@shaobo-he can this issue be closed or do you need more clarification?

[shaobo-he]

@shaobo-he can this issue be closed or do you need more clarification?

Thank you. Please close it. I think I have the information I needed.

[MartinSpiessl]

For the record: I just found out that CPAchecker indeed produces a returnFromFunction edge even if there is no return statement. In that case the statement we match is the function call site itself, not any particular line/ source code fragment inside the function.

I updated my post above #20 (comment) accordingly and added an example for future reference. I previously probably didn't spot this because we have the same line as Ultimate which renames the key to returnFrom, and I guess I originally only searched for FromFunction when scanning the witness for return edges.