Cleaning up SmackWarnings naming convention

[zvonimir]

I would like to clean up our naming convention in SmackWarnings since I think what we have now is confusing. So we have these 3 functions: warnUnModeled, warnIfIncomplete, warnImprecise.

I don't know what each of them means. Taking a step back, we have 3 cases:

• We encode something as an overapproximation. We should then have warnOverapproximate. This is when we are sound (we cannot miss bugs), but incomplete (we can have false bugs).
• We encode something as an underapproximation. We should then have warnUnderapproximate. This is when we are unsound (we can miss bugs), but complete (we cannot have false bugs).
• We encode something as neither an overapproximation nor an underapproximation. The encoding is basically wrong. For example, that can happen with our encoding of integer constants when bit-precise is not used. I don't have a good name for it yet. Also, when we simply drop inlined assembly, we have the same situation - we neither overapproximate it nor underapproximate. It is just wrong what we do.

Now I am curious how do our current names map to my proposed names?

[zvonimir]

@shaobo-he Could you help me out here please?

[zvonimir]

I get it! We should name them: warnOverApproximate, warnUnderApproximate, and warnApproximate!

[shaobo-he]

This issue has been fixed. Closed.