gauravpartha
gauravpartha
I agree. It's not clear to me whether one should do this before the AST reaches the backends. In Carbon, for example, it would be easy to report this using...
> > > Could the label invariant be encoded as an `assert ` in case the label is not a loop head? > > Anyway, in Prusti we currently encode...
If we allow while loops to exist that are not loop heads (I remember @dohrau mentioning that the CFG detection does not work properly then, so we should get his...
The order for field access was fixed in https://github.com/viperproject/carbon/pull/451.
> I guess to avoid this we'd either have to re-check well-definedness on unfold, or verify well-definedness using an unknown positive multiplicator? In general, yes. But I think there is...
I don't think it's an instance of #169, but rather an instance of #85. It seems that Carbon only supports multiplication of wildcards if it can be trivially determined that...
Still to be resolved: * in cases where something is inhaled or exhaled without definedness checks, because assertions have been checked to be self-framing elsewhere (specifications in method call and...
Possible optimization that has not yet been done: If precondition does not contain permissions, then do not need an uninterpreted guard function and instead can use the same approach as...
@marcoeilers Can one close this issue?
> > **@marcoeilers** commented on 2017-01-10 14:04 > > In some cases, well-definedness conditions are also apparently checked in the wrong order. For example, in the following code, in the...