search

runtimeverification / gitbook-kontrol

https://docs.runtimeverification.com/kontrol
4 stars 3 forks source link

Remove `infiniteGas` from example #15

Closed palinatolmach closed 8 months ago

palinatolmach commented 1 year ago

Infinite gas is now used by default in Kontrol, so providing kevm.infiniteGas() cheatcode is no longer necessary, so we should remove if from the example CounterTest contract we use in the documentation: https://docs.runtimeverification.com/kontrol/guides/kevm-foundry-integration-example/property-verification-using-kevm. The nodes corresponding to the kevm.infiniteGas() call will no longer be present in the KCFG, so it will require updates in the KCFG section too.

JuanCoRo commented 1 year ago

The status of this issue is that it explicitly says that the example of the infiniteGas() is merely for ilustration purposes since it's redundant to include it. Following #21, we should have a section on cheatocdes and create exples for the most used ones.

I think the only remaining action to do before closing the issue would be to update the screenshots for the code without the infiniteGas cheatcode, since that's the version that will stand.