Alexander Stekelenburg
Alexander Stekelenburg
Marking this as ready for review since I basically just want to add some tests now before merging this
Yeah so what I've done for now is simply detect which variables and fields get their address taken and "upgrade" those to pointers automatically. I'm not sure if there are...
> Looking at the code, you make a variable a pointer, whenever address of is used of that variable. Which is nice. > > I wonder how that works with...
Right now the following program can be verified: ```c struct A { int a; int b; }; struct B { struct A a; }; //@ ensures \result == 10; int...
An additional note about this: >To get this to work I had initialise the inner struct whenever the outer struct is initialised since otherwise you don't have permission to access...
Superseded by #1159
Yes this would be quite useful. Ideally there'd be a way we could give Viper a better view of which fields may alias and which may not instead of simply...
> 1. All fields of a struct are now stored in the same Viper field as pointer right? > So with `struct v {int x, int* xs}` v.x we get...
> I tried to better fix those decrease failures. Should close #1232 and #1065 So I guess you mean #1133 and #1065, since #1232 is the example you say was...
> The first one is harder to fix, since we get a single "decrease" clause from Viper as what was the reason. And I did not know how to redirect...