--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on June 2014 ---
Hello, I am using the wp plugin, and attempting to find the best way of dealing with separation logic. One situation I have come across is when using local variables. In the example below, the assertion is unknown, but I expect it to be valid since 'one' is valid prior to the function. /*@ requires \valid(one); */ void f(int *one){ int two; //@ assert one != &two; } Thanks for your time, Ian