bbyalcinkaya / k-javalette Goto Github PK

[Warning] Compiler: Potentially useless rule detected.
	Source(~/k-javalette/src/core/javalette-types.md)
	Location(167,10,167,35)
	167 |	    rule isLValue(_:Bool) => false
	    .	         ^~~~~~~~~~~~~~~~~~~~~~~~~
[Warning] Compiler: Potentially useless rule detected.
	Source(~/k-javalette/src/core/javalette-types.md)
	Location(168,10,168,34)
	168 |	    rule isLValue(_:Int) => false
	    .	         ^~~~~~~~~~~~~~~~~~~~~~~~
[Warning] Compiler: Potentially useless rule detected.
	Source(~/k-javalette/src/core/javalette-types.md)
	Location(169,10,169,36)
	169 |	    rule isLValue(_:Float) => false
	    .	         ^~~~~~~~~~~~~~~~~~~~~~~~~~
[Warning] Compiler: Potentially useless rule detected.
	Source(~/k-javalette/src/core/javalette-types.md)
	Location(170,10,170,37)
	170 |	    rule isLValue(_:String) => false
	    .	         ^~~~~~~~~~~~~~~~~~~~~~~~~~~

[Warning] Compiler: Potentially useless rule detected.
	Source(~/k-javalette/src/extensions/arrays.md)
	Location(166,10,166,39)
	166 |	    rule isLValue(_ . length) => false      [owise]
	    .	         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~

[Warning] Compiler: Potentially useless rule detected.
	Source(~/k-javalette/src/extensions/arrays.md)
	Location(102,9,104,29)
	    .	        v~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
	102 |	        <k> #elemAccess(array(Loc, Len), Ix) => X ...</k>
	103 |	        <store> ... (Loc +Int Ix ) |-> X ... </store>
	104 |	        requires Len >Int Ix
	    .	        ~~~~~~~~~~~~~~~~~~~^

[Warning] Compiler: Non exhaustive match detected:
`retcheckStmt(_)_JAVALETTE-RETURNCHECK_Bool_Stmt`(`if(_)__JAVALETTE-SYNTAX-CORE_Stmt_Exp_Stmt`(_,_))
	Source(~/k-javalette/src/core/javalette-returncheck.md)
	Location(32,21,32,57)
	32 |	    syntax Bool ::= retcheckStmt(Stmt) [function, total]
	   .	                    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
[Warning] Compiler: Non exhaustive match detected:
`isLValue(_)_JAVALETTE-TYPES_Bool_Exp`(`#elemAccess(_,_)_JAVALETTE-ARRAYS_Exp_Exp_Exp`(_,_))
	Source(~/k-javalette/src/core/javalette-types.md)
	Location(165,21,165,51)
	165 |	    syntax Bool ::= isLValue(Exp) [function,total]
	    .	                    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~