VeriFast Help > Error messages

Error message

Preciseness check failure: callee is not precise

Context

When checking the body of a precise predicate.

Cause

The body of a precise predicate mentions a non-precise predicate.

Notes

Suggested solutions

Suggested approaches:

• Change the callee to a precise predicate by placing a semicolon at the end of its parameters list.
• Change the predicate itself to a non-precise predicate by replacing the semicolon in the parameter list with a comma. Note that instance predicates are always precise and hence this solution does not apply to instance predicates.