runtimeverification / llvm-backend

KORE to llvm translation
BSD 3-Clause "New" or "Revised" License
34 stars 22 forks source link

`MInt` syntax with no uses of `Int2MInt` crashes #798

Open Baltoli opened 1 year ago

Baltoli commented 1 year ago

Compiling this code crashes the code generator; if the commented line is un-commented then it will compile and run correctly.

module TEST
  imports INT
  imports MINT

  syntax MInt{1}

  // rule _:Int => Int2MInt(0)::MInt{1}
endmodule

If the code is ill-formed for some reason when the rule is not present, we should emit a friendlier error message either in the frontend or in the backend.

Baltoli commented 1 year ago

This is a known bug; there's no reason it shouldn't work but is very low priority because there's no good reason to declare and not use one of these sorts.

Baltoli commented 1 year ago

Though @dwightguth comments that it's a confusing error for new users trying to experiment with MInt{...}; we should try and fix this.