explain why this function fails?

Apr 23, 2011 at 11:57 PM

int incm(int x)
{
  return unchecked(x+1);
}
int metric2(int i)
 requires(i<10)
ensures(result==i+1)
{   
    return incm(i);
}

whats the reason for this function failing ? 

P.S : I tried to verify metric2

Apr 26, 2011 at 9:23 AM
Edited Apr 26, 2011 at 10:42 AM

Well, for function calls VCC doesn't look into the function being called to determine its effect. All information is inferred from the function contract (read: post conditions / ensures clauses) of the called function being instantiated by the call parameters. 

Thus, as you haven't specified any post condition for 'incm', VCC does not "know" anything about the result of the function call when verifying 'metric2'. 

Apr 27, 2011 at 3:47 PM
Edited Apr 27, 2011 at 3:47 PM

thanks for reply

 

 

int incm(int x)

ensures(unchecked(x+1)
{
  return unchecked(x+1);
}
int metric2(int i)
 requires(i<10)
ensures(result==i+1)
{   
i=8;  

return incm(i);
}

why function failing when i am trying to assign some value to variable i like i=8 or something ?

Apr 27, 2011 at 7:30 PM

Hi metric,

what you are intending is probably sth like this ...

#include "vcc.h"

int incm(int x)
ensures (unchecked(result == x + 1))
{
    return unchecked(x + 1);
}

int metric2 (int i)
requires(i < 10)
ensures(result == i + 1)
{
    return incm(i);
}

Note that if you assign i = 8 in metric2 then you would violate the "ensures(result == i + 1)" for any i that is not 7, VCC will find a countermodel and not accept this a general theorem. Note to self: so far I have avoided "unsigned" and given how the requirement for "unchecked" taintedness gets lost in the postcondition (is that intended behavior or not) when calling "incm" from "metric2" that seems a good idea ...

Apr 27, 2011 at 7:42 PM

hmm yeah i didn't noticed , but i actually wrote like that in my visual studio .

and thanks for explanation on i=8 :)