Hover Refined Methods

[rcosta358]

Extend hover support to methods, similarly to variables (#70), by displaying their refinement information. This includes:

• Pre- and post-conditions (state refinements)
• Parameter refinements
• Return refinement

This will require some changes in the verifier to store this information in the context history.

Example

@StateRefinement(from="a()", to="b()")
@StateRefinement(from="b()", to="c()")
@Refinement("_ > 0")
int foo(@Refinement("_ > 1") int x) { ... }

Hovering foo (at definition or invocations) shows:

@StateRefinement(from="a()", to="b()")
@StateRefinement(from="b()", to="c()")
@Refinement("x > 1")
@Refinement("return > 0")