This project is read-only.

Funtion calls modify global variables

Mar 4, 2013 at 9:53 PM
Hi guys,

I have a problem with my code. The function calls will loss the informations about the global variables.
#include<vcc.h>
#include<stdlib.h>

_(ghost _(dynamic_owns) struct st {

} * s;)

void foo()
    //_(ensures \same(s))   //if uncomment this, the verify can be passed
;
void foo1()
    _(updates s)
{
    _(ghost \object t = s)
    foo();
    _(assert t == s)                //Assertion 't == s' did not verify.
    _(assert s \in \domain(s))
}

void foo2()
    _(maintains \wrapped(s))
{
    _(ghost \object t = s)
    foo();
    _(assert t == s)                //Assertion 't == s' did not verify.
    _(assert s \in \domain(s))
}

void foo3()
    _(updates s)
{
    _(ghost \object o = s)
    struct st * temp = (struct st *) malloc(sizeof(struct st));
    _(assert o == s)
    _(assert s \in \domain(s))
}
In this piece of code, I have a virtual struct st and its global point *s. The function foo1 -- foo3, call a function inside of them. For foo1, foo() is called, which do nothing with s, but the information about s is lost. I'm thinking foo1 have s in the writes clause, this may cause VCC thinking s may be modified by other function called by foo1. Therefore, in foo2(), I remove that. But VCC still lost the information of s. However, in foo3, malloc() is called, the information of global variable s keeps. Further, if I add the _(ensures \same(s)) to foo(), the information can be keep in foo1 and foo2.

In this simple case, it would be fine for me to add the post condition to functions to keep the global variables keep the same if it is not modified. However, for a larger case, it would be awful to do this.

I am wondering what is the post condition does malloc() have to make vcc keep the informations about s.

In Chapter 8 about atomic, I found, it is said the thread will forget the value of the object with volatile field. But I my struct don't have a field declared as volatile. Is the global variables be considered as volatile?

Does any one have any idea about this problem and how to solve this?

Thanks very much in advance.

Best Regards,

Shu Cheng
Apr 25, 2013 at 6:29 PM
Can no one have any idea about this? Or where can I found any resources about this?

Thanks very much!

Best,
Shu Cheng
Apr 26, 2013 at 7:00 PM
Hi,

your global pointer is a variable of primitive type and thus has an implicit object wrapped around it (cf. the previous discussion https://vcc.codeplex.com/discussions/405153). You can derive that the pointer stays the same if you reason with this enclosing object. For example, if you know the enclosing object is wrapped and not written to (by functions you call), you can derive that the pointer stays the same with explicitly mentioning it in functions such as foo().

Hope this helps, Mark
May 2, 2013 at 5:01 PM
Hi Mark,

Thanks very much for your reply.

The thread you mentioned is my another thread. I understand that and in the code here I also mentioned that if I have said something special in the post-condition for foo(), the proof would be fine. But my question is the system function calls, like malloc(), in the library, it is impossible to know which global variables I have in the code. In this case, it is impossible to state the pointers of global variables stay the same as post-condition for malloc(). And I'd like to know what happen here. Because if I have lots of global variables, it would be boring to have ensures clause for each of them to keep them unchanged.

Thanks very much.

Best,

Shu Cheng
May 2, 2013 at 6:54 PM
Hi,

sorry, in my earlier post, instead of "with explicitly mentioning [the object]" I meant "without explicitly mentioning [the object]". So foo() would stay without a postcondition. However, to take advantage of VCC framing, in foo1(), you would need to state something on the enclosing object of your global pointer 's', e.g.,
"_(requires \wrapped(\emb(&s)))". This would allow you to derive that 's' remains unchanged after foo() is called (even though the specification of foo() does not mention 's').

If I understand you correctly, foo() would correspond to malloc(), so this would be fine.

Hope that helps, Mark
May 2, 2013 at 8:12 PM
Hi Mark,

Thank you very much!!

It really helps! I confused "the context pointed by s" and "the pointer s itself" at the beginning. And I'm thinking for foo3(), I also didn't mention \gemb(&s) in the requirement. Why the function call of malloc() works properly in this function? This makes me confuse.

Thanks very much for helping.

Best Regards,

Shu Cheng