CODEWITHSUNDEEP
ada
agl
agl

Reputation: 1662

Compilation of ghost functions in SPARK 2014

I wish to abstract out some common patterns in pre and post conditions into a function in order to make the conditions more readable. From the documentation, it looks like ghost functions solve this issue.

I depend on the fact that overflows are eliminated in assertions (via a configuration pragma) so I don't believe that I can use ghost functions with code. The SPARK documentation contains the following example of a ghost function without code in http://docs.adacore.com/spark2014-docs/html/ug/spark_2014.html#ghost-functions :

function A_Nonexecutable_Ghost_Function (Lo, Hi : Natural) return Natural
with Pre        => Lo <= Hi,
     Post       => A_Nonexecutable_Ghost_Function'Result in Lo .. Hi,
     Convention => Ghost,
     Import;
-- The body of the function is not declared elsewhere.

However this, and any other ghost function like it that I try to write, results in:

warning: null global effect assumed on imported subprogram

And that warning stops compilation. Trying to say Global => () doesn't work. Can I suppress the warning? There's no obvious -Werror on the gnatprove command line that I can see to remove either.

Upvotes: 2

Views: 431

Answers (1)

ksson
ksson

Reputation: 168

The proper syntax is Global => null instead of Global => (), then the warning goes away.

Upvotes: 4

Related Questions