[Bug] [kompile] - kompile emits a "Non exhaustive match detected" warning for a seemingly sufficiently complete function definition
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 4/5
- Tempo stimato
- 3-5 giorni
- Idoneità per principianti
- 35/100
Direzione di ricerca
Inizia con l'esempio minimo in owise.k ed esegui kompile --syntax-module OWISE-SYNTAX owise.k per riprodurre l'avviso del verificatore di totalità. Traccia il modo in cui vengono analizzate le regole di foo, quindi conferma che la definizione funzionale sufficientemente completa non emetta più l'avviso senza la regola owise.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
K Version
$ kompile --version
K version: 5.2.97
Build date: Sun Mar 06 11:36:17 CST 2022
Description
kompile emits a "Non exhaustive match detected" warning seemingly unnecessarily in some cases (see the minimal example below). The function for which it gives the warning is declared functional and is sufficiently completely specified as far as I can tell.
Note: when uncommenting the owise line in the example below, the warning is not shown. But it shouldn't be needed, I think.
Input Files
The owise.k file below:
module OWISE-SYNTAX
syntax T ::= "uint"
syntax TList ::= List{T, ""} [klabel(list)]
endmodule
module OWISE
imports OWISE-SYNTAX
syntax MaybeT ::= T | "NoT"
syntax MaybeTList ::= List{MaybeT, ""} [klabel(list)]
syntax MaybeTList ::= TList
syntax MaybeTList ::= foo(MaybeTList) [function, functional]
// ---------------------------------------------------------
rule foo(.MaybeTList) => .MaybeTList
rule foo(_:MaybeT TL:MaybeTList) => uint foo(TL)
//rule foo(TL) => TL [owise] // to suppress a totality checker warning
endmodule
Reproduction Steps
kompile --syntax-module OWISE-SYNTAX owise.k
Expected Behavior
No "Non exhaustive match detected" warning is emitted.
- Lingua principale
- C++
- Stelle
- 43
- Fork
- 22
- Metriche di merge delle PR
- Nessuna PR unita negli ultimi 30g
Preparare l'ambiente
Questo progetto non fornisce container di sviluppo, Dockerfile né guida per i contributori, quindi l'ambiente è a tuo carico: parti dal suo README e consulta la nostra guida al primo contributo per i passaggi generali.
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di runtimeverification/llvm-backend
-
Difficoltà 1/5 Meno di un'ora Idoneità per principianti 84/100
runtimeverification/llvm-backend#1221 · 1 commento ·
-
code generation wontfix
Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100
runtimeverification/llvm-backend#1211 ·
-
bug garbage collection
Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100
runtimeverification/llvm-backend#1204 ·
-
Performance overhead in proof_trace_callback_writerForse già presa Una pull request collegata a questa issue è aperta o già unita. Aperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100
runtimeverification/llvm-backend#1197 · 1 commento ·
-
Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100
runtimeverification/llvm-backend#1196 ·
Tutte le issue di runtimeverification/llvm-backend
Issue simili
-
bug-unconfirmed
Difficoltà 2/5 1-3 ore Idoneità per principianti 70/100
I maintainer di solito rispondono entro 1 giorno
-
Extended search mode does not find escape sequences (\t, \n, \r...)Forse già presa @CyrilB1531 l’ha presa oggi. Aperta
Difficoltà 2/5 1-3 ore Idoneità per principianti 87/100
dail8859/NotepadNext#1181 ·
I maintainer di solito rispondono entro 1 giorno
-
A-tools P-low S-blocked task
Difficoltà 2/5 1-3 ore Idoneità per principianti 75/100
I maintainer di solito rispondono entro 1 giorno
-
☢️ Bug
Difficoltà 2/5 1-3 ore Idoneità per principianti 78/100
OpenAtomFoundation/pikiwidb#3309 ·
-
audit(c2): add_project_arguments('/experimental:c11atomics', language: ['c', 'cpp']) for MS (C2-13)Apertahygiene type:refactor
Difficoltà 2/5 1-3 ore Idoneità per principianti 66/100
I maintainer di solito rispondono entro 1 giorno