Skip to content

Commit

Permalink
Remove references to #parseKORE (#3701)
Browse files Browse the repository at this point in the history 
This PR removes all references to the deprecated `#parseKORE` hook

Paired with runtimeverification/k#3850,
runtimeverification/llvm-backend#919
  • Loading branch information
@Scott-Guest
Scott-Guest authored Dec 7, 2023
1 parent 0be07d2 commit a584730
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion test/issue-3508/definition.kore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -228,7 +228,7 @@ module IMP
hooked-symbol Lbl'Hash'open'LParUndsCommUndsRParUnds'K-IO'Unds'IOInt'Unds'String'Unds'String{}(SortString{}, SortString{}) : SortIOInt{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), impure{}(), hook{}("IO.open"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2408,18,2408,97)"), left{}(), format{}("%c#open%r %c(%r %1 %c,%r %2 %c)%r"), function{}()]
symbol Lbl'Hash'ostream'LParUndsRParUnds'K-IO'Unds'Stream'Unds'Int{}(SortInt{}) : SortStream{} [functional{}(), constructor{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("#ostream"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2589,21,2589,34)"), left{}(), format{}("%c#ostream%r %c(%r %1 %c)%r"), injective{}()]
symbol Lbl'Hash'parseInput'LParUndsCommUndsRParUnds'K-IO'Unds'Stream'Unds'String'Unds'String{}(SortString{}, SortString{}) : SortStream{} [functional{}(), constructor{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), klabel{}("#parseInput"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2588,21,2588,48)"), left{}(), format{}("%c#parseInput%r %c(%r %1 %c,%r %2 %c)%r"), injective{}()]
hooked-symbol Lbl'Hash'parseKORE'LParUndsRParUnds'K-REFLECTION'Unds'Sort'Unds'String{SortSort}(SortString{}) : SortSort [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("#parseKORE"), hook{}("KREFLECTION.parseKORE"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2265,26,2265,84)"), left{}(), format{}("%c#parseKORE%r %c(%r %1 %c)%r"), function{}()]
symbol Lbl'Hash'parseKORE'LParUndsRParUnds'K-REFLECTION'Unds'Sort'Unds'String{SortSort}(SortString{}) : SortSort [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("#parseKORE"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2265,26,2265,84)"), left{}(), format{}("%c#parseKORE%r %c(%r %1 %c)%r"), function{}(), no-evaluators{}()]
hooked-symbol Lbl'Hash'putc'LParUndsCommUndsRParUnds'K-IO'Unds'K'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortK{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), impure{}(), hook{}("IO.putc"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2447,16,2447,93)"), left{}(), format{}("%c#putc%r %c(%r %1 %c,%r %2 %c)%r"), function{}()]
hooked-symbol Lbl'Hash'read'LParUndsCommUndsRParUnds'K-IO'Unds'IOString'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortIOString{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), impure{}(), hook{}("IO.read"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2438,23,2438,99)"), left{}(), format{}("%c#read%r %c(%r %1 %c,%r %2 %c)%r"), function{}()]
hooked-symbol Lbl'Hash'remove'LParUndsRParUnds'K-IO'Unds'K'Unds'String{}(SortString{}) : SortK{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}(), priorities{}(), right{}(), terminals{}("1101"), impure{}(), klabel{}("#remove"), hook{}("IO.remove"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2541,16,2541,80)"), left{}(), format{}("%c#remove%r %c(%r %1 %c)%r"), function{}()]
Expand Down
2 changes: 1 addition & 1 deletion test/regression-c/test-smoke-definition.kore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1028,7 +1028,7 @@ module C
symbol Lbl'Hash'ostream'LParUndsRParUnds'K-IO'Unds'Stream'Unds'Int{}(SortInt{}) : SortStream{} [functional{}(), constructor{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("#ostream"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2487,21,2487,34)"), left{}(), format{}("%c#ostream%r %c(%r %1 %c)%r"), injective{}()]
symbol Lbl'Hash'parseInput'LParUndsCommUndsRParUnds'K-IO'Unds'Stream'Unds'String'Unds'String{}(SortString{}, SortString{}) : SortStream{} [functional{}(), constructor{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), klabel{}("#parseInput"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2486,21,2486,48)"), left{}(), format{}("%c#parseInput%r %c(%r %1 %c,%r %2 %c)%r"), injective{}()]
hooked-symbol Lbl'Hash'parseKAST'LParUndsRParUnds'K-REFLECTION'Unds'Sort'Unds'String{SortSort}(SortString{}) : SortSort [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("#parseKAST"), hook{}("KREFLECTION.parseKAST"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2173,26,2173,84)"), left{}(), format{}("%c#parseKAST%r %c(%r %1 %c)%r"), function{}()]
hooked-symbol Lbl'Hash'parseKORE'LParUndsRParUnds'K-REFLECTION'Unds'Sort'Unds'String{SortSort}(SortString{}) : SortSort [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("#parseKORE"), hook{}("KREFLECTION.parseKORE"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2171,26,2171,84)"), left{}(), format{}("%c#parseKORE%r %c(%r %1 %c)%r"), function{}()]
symbol Lbl'Hash'parseKORE'LParUndsRParUnds'K-REFLECTION'Unds'Sort'Unds'String{SortSort}(SortString{}) : SortSort [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("#parseKORE"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2171,26,2171,84)"), left{}(), format{}("%c#parseKORE%r %c(%r %1 %c)%r"), function{}(), no-evaluators{}()]
symbol Lbl'Hash'performDeferredChecks'LParRParUnds'C-CHECKER-SYNTAX'Unds'KItem{}() : SortKItem{} [functional{}(), constructor{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/c-semantics/semantics/checker/checker.k)"), priorities{}(), right{}(), terminals{}("111"), klabel{}("#performDeferredChecks"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(18,20,18,44)"), left{}(), format{}("%c#performDeferredChecks%r %c(%r %c)%r"), injective{}()]
symbol Lbl'Hash'pointerAdditionCheck'LParUndsCommUndsCommUndsRParUnds'C-ADDITIVE-EXP'Unds'KItem'Unds'ObjectId'Unds'Int'Unds'Type{}(SortObjectId{}, SortInt{}, SortType{}) : SortKItem{} [functional{}(), constructor{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/c-semantics/semantics/language/exp/additive.k)"), priorities{}(), right{}(), terminals{}("11010101"), klabel{}("#pointerAdditionCheck"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(39,20,39,62)"), left{}(), format{}("%c#pointerAdditionCheck%r %c(%r %1 %c,%r %2 %c,%r %3 %c)%r"), injective{}()]
symbol Lbl'Hash'promote'LParUndsCommUndsCommUndsRParUnds'C-CONVERSIONS'Unds'Exp'Unds'Exp'Unds'Type'Unds'MaybeInt{}(SortExp{}, SortType{}, SortMaybeInt{}, SortGeneratedTopCell{}) : SortExp{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/c-semantics/semantics/language/concepts/conversions.k)"), priorities{}(), right{}(), terminals{}("110101010"), klabel{}("#promote"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(98,18,98,58)"), left{}(), format{}("%c#promote%r %c(%r %1 %c,%r %2 %c,%r %3 %c)%r %4"), function{}()]
Expand Down

0 comments on commit a584730

Please sign in to comment.