Ability to initialize parametrized constructor

[dearzubi]

In our smart contracts, there are several properties dependent on the state variables which need to be initialized through the constructor. In one such instance, we need to check that "msg.value" is always greater than a global state variable value "Rv" during a call to the "registerEntity" function. The value of "Rv" is initialized through the constructor. Now, if we use "Rv" in the specification language of scribble the property never succeeds because "Rv" is by default 0.

So, is there any way we can initialize constructor parameters with hardcoding them inside the constructor? Maybe there could be something like VerX provides: VerX

[cd1m0]

I am not sure if I understand everything here. If you just want to check that msg.value > Rv JUST BEFORE the registerEntity function, you can do something like this:

/// #if_succeeds old(msg.value>Rv);
function registerEntity(....) {
   ...
}

[cd1m0]

Does this answer your question? Or is it something different?

[cd1m0]

Haven't heard anything on this for a while, so closing. If this is still an issue please reopen