Can boogie verify the function calling sequence?

[ya0guang]

Actually I'm using smack, a verifier for C/C++ which uses Boogie language and support inline Boogie, to do a research project about software security.
I want to verify my program will execute as what I expected: function call will return to a place where it is called and some functions will be executed in a certain sequence in my program. Can Boogie verify this?
I've checked The Boogie IVL language reference but I cannot find a anwser to my question, and it seems the document is far from complete. So I also checked This is Boogie 2. I found trace is an important conception in Boogie, and I found procedure might be useful in my task. However, I got confused and don't know where to start with: I can find few examples about my requirement.
Could you please give me a small example of how to specify such a thing in Boogie: ensuring a function call will return to a certain place.

procedure Foo() returns ();
  //ensures returning to Bar()

procedure Bar() returns ();
{
  //do_something();
  //call Foo();
  //do_something()
}

Thanks a lot.

[zvonimir]

Hi there. I am not sure what you mean by "function call will return to a place where it is called". In Boogie, procedures always return to the place where they were called, and so checking something like that would not make sense - the language semantics ensures that.

I would guess that in the context of security and C programs, this might not be the case since one could tamper with the call stack. Is that what you are trying to check?

I think it would probably be better if you would create an issue on the SMACK GitHub page and explain there what you would like to achieve at the level of C (not Boogie). Then we could hopefully help you out there.

[ya0guang]

@zvonimir
Thank you for replying me! Actually I'm considering the situation in which the return address might be modified while a function is being executed. When the return address located in stack is messed up, the function may not return to the place where it was called.
Although SMACK has "--memory-safety" flag, it seems SMACK can NOT guarantee the source code is free of memory-bug. So I had a glance at SMACK's source code and found that you build your memory model on your own and use Boogie assertion to assert memory safety. Thus, I came here and want to find out if there will be a solution for my problem using the Boogie, since solving the problem may require us to build a stack model in Boogie for function call. Also, SMACK does not model stack behaviors (At least I didn't see in the memory model description in smack.c) because of the lack of expressiveness of stack opreation in C.
If you still think it's better to open an issue in SMACK, I'll describe my question again with more details there.
Again, thanks a lot!

[zvonimir]

Thanks for the clarification. In my opinion, the appropriate place for addressing this would be in SMACK, and not Boogie. The way to do it, and this would require some work, would be to introduce the model of the call stack in the Boogie files generated by SMACK.

So you should probably open an issue in the SMACK repo about this. It would also be great if you could add an example that illustrates what you would like to achieve.