Skip to content

Commit

Permalink
Fix regression tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@Baltoli
Baltoli committed Feb 26, 2024
1 parent 6478f8e commit 2495800
Show file tree
Hide file tree
Showing 13 changed files with 40 additions and 40 deletions.
2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/bison-glr-bug/iele.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ module IELE-COMMON
syntax IeleName ::=
IeleNameToken
syntax IeleName ::=
StringIeleName [avoid, function, klabel(StringIeleName), symbol]
StringIeleName [avoid, function, symbol(StringIeleName)]
syntax GlobalName ::=
"@" IeleName
syntax LocalName ::=
Expand Down
4 changes: 2 additions & 2 deletions k-distribution/tests/regression-new/checkWarns/missingKlabel.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,10 +7,10 @@ module MISSINGKLABEL
imports BASIC-K

syntax MyMap ::= KItem "M|->" KItem
[ function, total, hook(MAP.element), klabel(_M|->_), symbol, injective, unused]
[ function, total, hook(MAP.element), symbol(_M|->_), injective, unused]

syntax MyMap ::= MyMap MyMap
[ left, function, hook(MAP.concat), klabel(_MyMap_), symbol, assoc, comm
[ left, function, hook(MAP.concat), symbol(_MyMap_), assoc, comm
, unit(.MyMap), element(_M|->_), index(0), format(%1%n%2), unused
]

Expand Down
2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/context-alias-2/test.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ module TEST
| Id "=" Int
| Id
| Int
| l(Exp) [klabel(l), symbol] | m(Exp) [klabel(m), symbol] | r(Exp) [klabel(r), symbol]
| l(Exp) [symbol(l)] | m(Exp) [symbol(m)] | r(Exp) [symbol(r)]
syntax KResult ::= Int

context alias [left]: HERE [context(l)]
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/issue-1263/test.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ module TEST

configuration <k> $PGM:Pgm </k>

syntax FInt ::= FInt ( value: Int , one: Int ) [klabel(FInt), symbol]
syntax FInt ::= FInt ( value: Int , one: Int ) [symbol(FInt)]
// ---------------------------------------------------------------------

syntax Wad = FInt
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/issue-1273/test.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ module TEST
imports BOOL

syntax FInt ::= "(" FInt ")" [bracket]
| FInt ( value: Int , one: Int ) [klabel(FInt), symbol]
| FInt ( value: Int , one: Int ) [symbol(FInt)]
// ---------------------------------------------------------------------

syntax FInt ::= "1FInt" "(" Int ")" [macro]
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/issue-1682-korePrettyPrint/test.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,5 +4,5 @@ module TEST
syntax X ::= "a"
configuration <k> $PGM:X </k>
rule <k> a => ?_:Int </k>
syntax Bool ::= pred1 ( Int ) [function, total, klabel(pred1), symbol, no-evaluators]
syntax Bool ::= pred1 ( Int ) [function, total, symbol(pred1), no-evaluators]
endmodule
24 changes: 12 additions & 12 deletions k-distribution/tests/regression-new/issue-1760/test.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,13 +18,13 @@ module TEST
// Boolean Algebra Part of KAT

syntax Kat ::= Bool
| "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), hook(KAT.not)]
> Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), group(boolOperation), hook(KAT.and)]
| Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)]
| Kat "=/=Kat" Kat [function, total, klabel(_=/=Kat_), symbol, left, smt-hook(distinct), hook(KAT.ne)]
//| Kat "impliesKat" Kat [function, total, klabel(_impliesKat_), symbol, left, smt-hook(=>), group(boolOperation), hook(KAT.implies)]
| "notKat" Kat [function, total, symbol(notKat_), smt-hook(not), group(boolOperation), hook(KAT.not)]
> Kat "andKat" Kat [function, total, symbol(_andKat_), left, smt-hook(and), group(boolOperation), hook(KAT.and)]
| Kat "orKat" Kat [function, total, symbol(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)]
| Kat "=/=Kat" Kat [function, total, symbol(_=/=Kat_), left, smt-hook(distinct), hook(KAT.ne)]
//| Kat "impliesKat" Kat [function, total, symbol(_impliesKat_), left, smt-hook(=>), group(boolOperation), hook(KAT.implies)]

syntax Bool ::= Kat "==Kat" Kat [function, total, klabel(_==Kat_), symbol, left, smt-hook(=), hook(KAT.eq)]
syntax Bool ::= Kat "==Kat" Kat [function, total, symbol(_==Kat_), left, smt-hook(=), hook(KAT.eq)]


syntax Kat ::= freshKat(Kat) [freshGenerator, function]
Expand Down Expand Up @@ -66,19 +66,19 @@ module TEST
/*
syntax Kat ::= "(" Kat ")" [bracket]
> left:
Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), hook(KAT.mul)]
Kat "Kat*" [function, symbol(_starKat), left, smtlib(ka_star), hook(KAT.mul)]
> left:
Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), hook(KAT.seq)]
Kat "Kat;" Kat [function, symbol(_seqKat_), left, smtlib(ka_seq), hook(KAT.seq)]
> left:
Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), hook(KAT.pll)]
Kat "Kat|" Kat [function, symbol(_pllKat_), left, smtlib(ka_pll), hook(KAT.pll)]

*/

syntax Kat ::= "(" Kat ")" [bracket]
> left:
Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), hook(KAT.mul)]
| Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), hook(KAT.seq)]
| Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), hook(KAT.pll)]
Kat "Kat*" [function, symbol(_starKat), left, smtlib(ka_star), hook(KAT.mul)]
| Kat "Kat;" Kat [function, symbol(_seqKat_), left, smtlib(ka_seq), hook(KAT.seq)]
| Kat "Kat|" Kat [function, symbol(_pllKat_), left, smtlib(ka_pll), hook(KAT.pll)]


rule ONE Kat; B:Kat => B:Kat
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/issue-1879-kproveTrans/haskell/test.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ module TEST
syntax Step ::= Int
// -------------------

syntax FInt ::= FInt ( value: Int , one: Int ) [klabel(FInt), symbol]
syntax FInt ::= FInt ( value: Int , one: Int ) [symbol(FInt)]
// ---------------------------------------------------------------------

syntax FInt ::= "0FInt" "(" Int ")" [macro]
Expand Down
8 changes: 4 additions & 4 deletions k-distribution/tests/regression-new/issue-2321-kprovexCrash/test.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,17 +4,17 @@ module TEST
imports INT

syntax Exp ::= Int | Bool
| pair(Int, Int) [klabel(pair), symbol]
| pair(Int, Int) [symbol(pair)]

syntax KItem ::= "#assume" Exp [klabel(assume), symbol]
syntax KItem ::= "#assume" Exp [symbol(assume)]
rule #assume true => .K
rule #assume false => #Bottom

syntax KItem ::= "#assert" Exp [klabel(assert), symbol]
syntax KItem ::= "#assert" Exp [symbol(assert)]
| "#fail"
rule #assert true => .K
rule #assert false => #fail

// Uninterpreted functions
syntax Int ::= i(Int, Int) [function, total, no-evaluators, smtlib(fi), klabel(i)]
syntax Int ::= i(Int, Int) [function, total, no-evaluators, smtlib(fi), symbol(i)]
endmodule
24 changes: 12 additions & 12 deletions k-distribution/tests/regression-new/issue-999/kat.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,13 +18,13 @@ module KAT
// Boolean Algebra Part of KAT

syntax Kat ::= Bool
| "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), hook(KAT.not)]
> Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), group(boolOperation), hook(KAT.and)]
| Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)]
| Kat "=/=Kat" Kat [function, total, klabel(_=/=Kat_), symbol, left, smt-hook(distinct), hook(KAT.ne)]
//| Kat "impliesKat" Kat [function, total, klabel(_impliesKat_), symbol, left, smt-hook(=>), group(boolOperation), hook(KAT.implies)]
| "notKat" Kat [function, total, symbol(notKat_), smt-hook(not), group(boolOperation), hook(KAT.not)]
> Kat "andKat" Kat [function, total, symbol(_andKat_), left, smt-hook(and), group(boolOperation), hook(KAT.and)]
| Kat "orKat" Kat [function, total, symbol(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)]
| Kat "=/=Kat" Kat [function, total, symbol(_=/=Kat_), left, smt-hook(distinct), hook(KAT.ne)]
//| Kat "impliesKat" Kat [function, total, symbol(_impliesKat_), left, smt-hook(=>), group(boolOperation), hook(KAT.implies)]

syntax Bool ::= Kat "==Kat" Kat [function, total, klabel(_==Kat_), symbol, left, smt-hook(=), hook(KAT.eq)]
syntax Bool ::= Kat "==Kat" Kat [function, total, symbol(_==Kat_), left, smt-hook(=), hook(KAT.eq)]


syntax Kat ::= freshKat(Kat) [freshGenerator, function]
Expand Down Expand Up @@ -66,19 +66,19 @@ module KAT
/*
syntax Kat ::= "(" Kat ")" [bracket]
> left:
Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), hook(KAT.mul)]
Kat "Kat*" [function, symbol(_starKat), left, smtlib(ka_star), hook(KAT.mul)]
> left:
Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), hook(KAT.seq)]
Kat "Kat;" Kat [function, symbol(_seqKat_), left, smtlib(ka_seq), hook(KAT.seq)]
> left:
Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), hook(KAT.pll)]
Kat "Kat|" Kat [function, symbol(_pllKat_), left, smtlib(ka_pll), hook(KAT.pll)]

*/

syntax Kat ::= "(" Kat ")" [bracket]
> left:
Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), hook(KAT.mul)]
| Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), hook(KAT.seq)]
| Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), hook(KAT.pll)]
Kat "Kat*" [function, symbol(_starKat), left, smtlib(ka_star), hook(KAT.mul)]
| Kat "Kat;" Kat [function, symbol(_seqKat_), left, smtlib(ka_seq), hook(KAT.seq)]
| Kat "Kat|" Kat [function, symbol(_pllKat_), left, smtlib(ka_pll), hook(KAT.pll)]


rule ONE Kat; B:Kat => B:Kat
Expand Down
2 changes: 1 addition & 1 deletion ...ession-new/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,7 @@ the wrapper in the generated documentation, we associate it an

```k
syntax Type ::= "void" | "int" | "bool" | "string"
| Id [klabel("class"), symbol, avoid] // see next
| Id [symbol("class"), avoid] // see next
| Type "[" "]"
| "(" Type ")" [bracket]
> Types "->" Type
Expand Down
2 changes: 1 addition & 1 deletion ...ession-new/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -350,7 +350,7 @@ a constructor for function types:
| "(" Type ")" [bracket]
| TypeVar
| TypeName [klabel(TypeName), avoid]
| Type TypeName [klabel(Type-TypeName), symbol, macro]
| Type TypeName [symbol(Type-TypeName), macro]
| "(" Types ")" TypeName [prefer]
syntax Types ::= List{Type,","} [klabel(types)]
syntax Types ::= TypeVars
Expand Down
4 changes: 2 additions & 2 deletions k-distribution/tests/regression-new/unparseKORE/test.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ module TEST

syntax A ::= "a1" A
| "a2" A
| "a1" [klabel(b1), symbol]
| "a2" [klabel(a2), symbol]
| "a1" [symbol(b1)]
| "a2" [symbol(a2)]

rule a1 => #unparseKORE(a1)
rule a2 => #unparseKORE(a2)
Expand Down

0 comments on commit 2495800

Please sign in to comment.