Handle pseudo return node in CFG comparison

[sim642]

This issue appeared in https://github.com/goblint/analyzer/pull/542#issuecomment-1023077417, but previously happened to be accidentally hidden by some hashtable having keys stored and iterated in a different order.

If the old function had no return statement and a pseudo return node was inserted, but the new function has an explicit return; inserted at the end, then when their CFGs are compared incrementally, no differences will be found and the function goes into unchanged. But then a crash occurs here: https://github.com/goblint/analyzer/blob/84c1ef9f3f05771f6211e6517fc538847ef20fe6/src/incremental/updateCil.ml#L48 Because the pseudo return node (and its statement) is not part of old_f.sallstmts, but the equivalent return node is in f.sallstmts, so the unchanged function has a different number of statements.

The CFG comparison probably also needs to exclude pseudo return nodes and consider them different. At least as long as the pseudo return node isn't added to sallstmts (for which there was some reason for not doing that).

---

A follow-up question: if two functions have different ASTs, but same CFGs and hence end up in unchanged, what guarantee is there that UpdateCil.update_ids.reset_fun works at all? Couldn't two equivalent functions have different statements lists. For example, one having extra Blocks for no reason, which don't change the CFG. Also, even when such thing does not happen, why can it be assumed that the statements correspond exactly in that order? Shouldn't the node correspondence constructed by CFG comparison be used in that case to update the sids?

[sim642]

As found by @michael-schwarz, there seems to be a closely related issue: https://github.com/goblint/bench/issues/16#issuecomment-1023440349. But that one is crashing on the iteration of slocals, not sallstmts. I suppose there's also the possibility that the difference is in the locals (which maybe are unused). That wouldn't affect the function's signature (unchangedHeader).