#[kani::proof_for_contract] rejects multiple contracts for the same proof

[zjp-CN]

error: Failed to resolve checking function contract_requires, contract_ensures because Expected a path, but found `contract_requires, contract
_ensures`. unexpected token
  --> tests/proofs/proofs_for_contract.rs:21:5
   |
21 |     #[kani::proof_for_contract(contract_requires, contract_ensures)]
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: this error originates in the attribute macro `kani::proof_for_contract` (in Nightly builds, run with -Z macro-backtrace for more in
fo)

error: Failed to resolve `contract_requires, contract_ensures` for `proof_for_contract`: Expected a path, but found `contract_requires, contra
ct_ensures`. unexpected token
  --> tests/proofs/proofs_for_contract.rs:22:5
   |
22 |     fn two_contracts_requires_and_ensures() {
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[zjp-CN]

And if no contract specified in the proof, it won't compile:

error: The function specified in the `proof_for_contract` attribute, `contract_requires`, was not found.
       Make sure the function is reachable from the harness.
  --> tests/proofs/proofs_for_contract.rs:21:5
   |
21 |     #[kani::proof_for_contract(contract_requires)]
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |

Nice.