Correctness-Guaranteed Code Generation via Constrained Decoding