Better visualize proofs for assertions inserted by SpecificationChecker

[leonhandreke]

SpecificationChecker inserts some assertions into a program that are directly related to a syntax element but are not inserted into the code. An example for this is the "division by zero" check inserted before every division.

These proofs should show up in the UI and color the appropriate related syntax element according to the outcome of the proof.

[jspam]

There is not much the UI can do about this. It gets passed the implicit assertion inserted by the prover, but it cannot mark it because there is no corresponding parse tree node in the source file.

My suggestion for this is creating a new subclass DivisorNotZeroAssertion of Assertion in the model, which has an additional property checkedExpression pointing e.g. to a BinaryExpression (which can be a division or modulo). This special type of assertion would be inserted by the prover instead of a normal _assert.

IProverEventListener would then have another event, named along the lines of divisorNotZeroVerified, which would get the failed expression (not the assertion) as a parameter.

The prover could chose whether to call this event only in the case of an annotation failure, or always.

[leonhandreke]

Yes, I think that would be the best approach. Could you add DivisorNotZeroAssertion and FunctionCallPreconditionAssertion to the model (I'm not very good with this EMF stuff). I would then implement your suggestions based on these classes.

[jspam]

Done in c5365b2. I think the distinction betweeen DivisorNotZeroAssertion and FunctionCallPreconditionAssertion is not necessary (or is it?), so I created a single model element called GuardAssertion (imagine this).

[jspam]

Oh well, I figured out you might indeed need two separate assertions, so I subclassed GuardAssertion and added the two new assertion types, too.

[jspam]

You can assign the issue to me when you’re finished.