Repository navigation
Context tab shows refinements differently from the error messages (state shorthand, host#1, #switch_selector) #184
Description
With verifier 0.0.37 the error messages show refinements differently from the Context tab, so the two views of the same variable disagree.
What the Context tab shows
| Error message (0.0.37) | Context tab (main) | |
|---|---|---|
| States of a named set | display(host) == notDisplayable, stream(buffered) == open (liquid-java/liquidjava#511) |
notDisplayable(host), open(buffered) && unmarked(buffered) |
| Variables written alike | the declared variable plain, other values host@23 (the line the value comes from) |
six rows all named host, and host == host#1 |
| Values the verifier introduces | inlined where they stand for one expression | #switch_selector == newMode, length(data) == #array_length, #array_length == 1024, #if_condition |
A1_09 and A1_38 (proposal D):
host#1, #switch_selector and #array_length are never explained to a novice, and #if_condition | #if_condition says nothing.
Fix
Have the server format the context the way the error messages are formatted, with the verifier's public API (no verifier change needed):
StateValues.toSetFormfor the states of named sets;- one
DisplayNamesfor the context, withContextHistory.lineOf, so a value is calledhost@23as in error messages; - the values the verifier introduces (
##...) are not listed as variables; one that stands for a single expression (#array_length == 1024) is replaced by it, and a comparison with one that is not constrained at all (cff == #getFileFilter_result) is left out.
The Ghosts section has the same problem (#177): states of a named set are listed as boolean compressionExplicit(ImageWriteParam) ghost. They should be compression(ImageWriteParam) == compressionExplicit, kind state.
Activity