Warn when a claim is proven without taking any steps

[andreiburdusa]

---

Fixes #1869

Reviewer checklist

• Test coverage: stack test --coverage
• Public API documentation: stack haddock

[andreiburdusa]

I runed a-to-c-spec.k from tiny using --dry-run. This is spec.kore:

[]
module A-TO-C-SPEC

// imports
import VERIFICATION []


// claims
// rule `<generatedTop>`(`<k>`(inj{S,KItem}(`a_TINY_S`(.KList))~>_DotVar1),_DotVar0)=>`<generatedTop>`(`<k>`(inj{S,KItem}(`c_TINY_S`(.KList))~>_DotVar1),_DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8), contentStartLine(9), org.kframework.attributes.Location(Location(9,8,9,14)), org.kframework.attributes.Source(Source(/home/andrei/kore/test/tiny/././a-to-c-automatic-repl-script-spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
  claim{} \implies{SortGeneratedTopCell{}} (
      \and{SortGeneratedTopCell{}} (
      \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortS{}, SortKItem{}}(Lbla'Unds'TINY'Unds'S{}()),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})), weakAlwaysFinally{SortGeneratedTopCell{}} (
      \and{SortGeneratedTopCell{}} (
      \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortS{}, SortKItem{}}(Lblc'Unds'TINY'Unds'S{}()),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}))))
  [org'Stop'kframework'Stop'attributes'Stop'Source{}(), org'Stop'kframework'Stop'definition'Stop'Production{}(), contentStartLine{}(), contentStartColumn{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}()]

endmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}()]

The only line that contains a location is commented (// rule `<generatedTop>`...)