search

makerdao / mkr-mcd-spec

High level KSpecification for the MCD System by Runtime Verification and Maker Foundation
GNU General Public License v3.0
28 stars 9 forks source link

Test Harness Vat Line #194

Closed andy8052 closed 4 years ago

andy8052 commented 4 years ago

The test harness code being generated seems to always use Line when calling file in the vat. While Line is correct for a 2 parameter file call, it should be line when call with 3. This can be seen here. I looked at the python code to change it myself but it will probably take someone on the RV team 1/10 the time as I have not really ever looked at this python code. Happy to dive in though if we want me to.

kmbarry1 commented 4 years ago

cc @ehildenb

Yeah, the K code looks correct, seems to be an issue with the Solidity generation instead.