dapphub / klab

K framework proof explorer & smart contract specification format
GNU Affero General Public License v3.0
123 stars 36 forks source link

Format fix #420

Closed kmbarry1 closed 4 years ago

kmbarry1 commented 4 years ago

kast.format is used to format gas expressions for use in pass specifications; recent changes (see #413) introduced changes that make the output of format unparseable by K.

This PR introduces a variable that can be used to differentiate between pretty-printing and generating valid K syntax for use in specifications, and applies it conservatively to prevent issues (i.e. there may be other situations in which it should be used, I didn't try to be exhaustive here).