Broken Support for Functions Without Parameters

[Heizmann]

Functions without parameters are legal in Boogie (see Section 3 of "This is Boogie 2" https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml178.pdf)

Boogie and die ICFG distinguish between constants and functions. In SMT-LIB constants and 0-ary functions coincide.

The construction algorithm of the Transformula fails because it expects that "myFunction" is a constant.

[danieldietsch]

I do not see the connection to #442.

We are currently translating this function to a 0-ary SMT function: (declare-fun myFunction () Int) Do you propose that we identify 0-ary functions and translate them to constants, i.e., (declare-const myFunction Int)? From an SMT perspective, this does not change anything.

Or are you proposing to fix the construction algorithm of the Transformula?

[Heizmann]

The only connection to #442 that I can see is what I mentioned there: I failed to reproduce the problem of #442 because of this issue.

In SMT-LIB 0-ary functions are constants. The declare-const command is just syntactic sugar for a declare-fun command with zero parameters.

I do/did not propose a solution.

My main concern is that I implemented everything without considering this problem. Other manifestations of this problem might be more severe and might not be captured by a failing assert statement. Maybe we should just let the RCFG Builder produce an UnsupportedSyntax result that refers to this issue and wait until we have more examples

(One way to produce more examples: Let the CACSLTranslator translate every global variable that is not modified in any procedure into an 0-ary boogie function. Compare the verification results with the results for the original translation.)