Script-friendly output

[Ef55]

The summary produced by Stainless is really good from a human-readability standpoint, but the same cannot be said from the parsing standpoint. The --no-colors flag already improves this a lot, but there are two remaining issues:

• There is additional data printed around the summary;
• There is no easy way of splitting the different columns.

An example:

Starting verification...
Verified: 2 / 7
warning:  - Result for 'precond. (call ackermann(m - BigInt("1"), ackermann(...)' VC for ackermann @11:7:
warning: m < BigInt("0") || n < BigInt("0") || m == BigInt("0") || n == BigInt("0") || m - BigInt("1") >= BigInt("0") && ackermann(m, n - BigInt("1")) >= BigInt("0")
test.scala:11:7: warning:  => TIMEOUT
                 ackermann(m - 1, ackermann(m, n - 1))
                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Verified: 6 / 7

 stainless summary 

test.scala:2:3:     ackermann  non-negative measure                                      valid    U:smt-z3  0.0 
test.scala:8:7:     ackermann  measure decreases                                         valid    U:smt-z3  0.0 
test.scala:8:7:     ackermann  precond. (call ackermann(m - BigInt("1"), BigInt("1")))   valid    U:smt-z3  0.1 
test.scala:11:7:    ackermann  measure decreases                                         valid    U:smt-z3  0.0 
test.scala:11:7:    ackermann  precond. (call ackermann(m - BigInt("1"), ackermann(...)  timeout  U:smt-z3  1.1 
test.scala:11:24:   ackermann  measure decreases                                         valid    U:smt-z3  0.0 
test.scala:11:24:   ackermann  precond. (call ackermann(m, n - BigInt("1")))             valid    U:smt-z3  0.0 
.................................................................................................................
total: 7    valid: 6    (0 from cache) invalid: 0    unknown: 1    time:     1.3  

The best solution I found is to apply

_.dropWhile(!_.contains("stainless summary")).tails.dropRight(2)

to extract the summary lines, and then parse the lines with the extremely ad hoc and brittle:

val whiteSpaces = """\p{Blank}+"""
val resultRegex = """((?:valid from cache)|(?:valid)|(?:timeout))"""
val template = s"""([\\w/:\\\\.]*)${whiteSpaces}(\\w*)${whiteSpaces}(.*)${whiteSpaces}${resultRegex}${whiteSpaces}(?:nativez3${whiteSpaces})?([\\d\\\\.]*)${whiteSpaces}"""
val regex = java.util.regex.Pattern.compile(template).matcher(vc)

A possible solution would be to add a new flag which:

• Suppress everything but the summary. If one wants to include extra information lines (e.g. the "one-line summary at the end"), print them before the summary (and always the same number of lines) so that they can easily be dropped;
• Somehow separate the columns (a possibility would be with commas, as to basically get the csv format, but the middle column can contains commas, so another character might be better).

As an added bonus, it would also be nice to then have a specification of the format of the different columns.

Note: there might be overlap between what I'm describing here and the JSON output option.

[vkuncak]

These are good suggestions. We could likely use semicolon to as the column separator. I think summary is quite important, so it would be good to discuss how to denote the end of individual VC outcomes and the beginning of a summary line.