SMACK currently does not support inttoptr. Instead it reports "Instruction not handled" and terminates. Add simple support for inttoptr by translating it into a simple assignment statement.

Currently there is no support for functions that return a structure.
Hence, this example is failing (see example/failing/struct_return.c):

#include "smack.h"

struct a {
  long i;
  long j;
};

struct a foo(struct a bar) {
  bar.i = 10;
  bar.j = 20;
  return bar;
}

int main(void) {
  struct a x;
  x = foo(x);
  __SMACK_assert(x.j == 20);
  return 0;
}

I am unable to figure out why the following program verifies (on rise4fun).

include "smack.h"

define SIZE 2

//init
int memInit[SIZE];
int cacheDataInit;
int outInit;

int main(void) {
int precise = __SMACK_nondet();
__SMACK_assume(precise >= 0 && precise < SIZE);
int cacheAddr = 0;
int cacheData = 0;
int mem[SIZE];
for (int i = 0; i < SIZE; i++) { mem[i] = memInit[i]; }
int out = 0;
__SMACK_assert(false);
return 0;
}

We should implement FunExpr class, which would be used for calling functions (i.e., for function expressions) in Boogie. PtrArithExpr would then become a subclass of FunExpr, as well as P2IExpr, I2PExpr, and so on.
I am still not sure what fields FunExpr would have (probably function name?). But this seems like a reasonable restructuring.

The following crashes smackgen.py due to the clangOutput variable only being defined when a .c file is given as input.

$ smackgen.py simple.bc -o simple.bpl
Traceback (most recent call last):
  File "/usr/local/bin/smackgen.py", line 117, in <module>
    bpl, options, clangOutput = smackGenerate(sys.argv)
  File "/usr/local/bin/smackgen.py", line 108, in smackGenerate
    return bpl, options, clangOutput
UnboundLocalError: local variable 'clangOutput' referenced before assignment

OS: MAC OS X 10.8.3

configure: creating ./config.status
config.status: creating Makefile.common
config.status: creating Makefile.llvm.config
config.status: executing setup commands
config.status: executing Makefile commands
./config.status: line 1065: /Users/pgbi/autoconf/mkinstalldirs: No such file or directory
/bin/sh: /Users/pgbi/autoconf/install-sh: No such file or directory
config.status: executing lib/Makefile commands
./config.status: line 1067: /Users/pgbi/autoconf/mkinstalldirs: No such file or directory
/bin/sh: /Users/pgbi/autoconf/install-sh: No such file or directory
config.status: executing lib/smack/Makefile commands
./config.status: line 1069: /Users/pgbi/autoconf/mkinstalldirs: No such file or directory
/bin/sh: /Users/pgbi/autoconf/install-sh: No such file or directory

$ make install
llvm[0]: Installing include files
/usr/bin/install: ‘./Exprs.h’ and ‘/home/sergio/smack/include/./Exprs.h’ are the same file
/usr/bin/install: ‘./BplPrintUtils.h’ and ‘/home/sergio/smack/include/./BplPrintUtils.h’ are the same file
/usr/bin/install: ‘./SmackInstVisitor.h’ and ‘/home/sergio/smack/include/./SmackInstVisitor.h’ are the same file
/usr/bin/install: ‘./Utils.h’ and ‘/home/sergio/smack/include/./Utils.h’ are the same file
/usr/bin/install: ‘./Common.h’ and ‘/home/sergio/smack/include/./Common.h’ are the same file
/usr/bin/install: ‘./Memory.h’ and ‘/home/sergio/smack/include/./Memory.h’ are the same file
/usr/bin/install: ‘./SmackGenerator.h’ and ‘/home/sergio/smack/include/./SmackGenerator.h’ are the same file
/usr/bin/install: ‘./SmackModule.h’ and ‘/home/sergio/smack/include/./SmackModule.h’ are the same file
/usr/bin/install: ‘./BplPrinter.h’ and ‘/home/sergio/smack/include/./BplPrinter.h’ are the same file
/usr/bin/install: ‘./Statement.h’ and ‘/home/sergio/smack/include/./Statement.h’ are the same file
/usr/bin/install: ‘./Expr.h’ and ‘/home/sergio/smack/include/./Expr.h’ are the same file
/usr/bin/install: ‘./Block.h’ and ‘/home/sergio/smack/include/./Block.h’ are the same file
/usr/bin/install: ‘./Statements.h’ and ‘/home/sergio/smack/include/./Statements.h’ are the same file
/usr/bin/install: ‘./Procedure.h’ and ‘/home/sergio/smack/include/./Procedure.h’ are the same file
make: *** [install-local] Error 1

The following crashes llvm2bpl.py. One wonders whether there is a way NOT TO crash llvm2bpl.py :-)

$ llvm2bpl.py simple.bc
Traceback (most recent call last):
  File "/usr/local/bin/llvm2bpl.py", line 62, in <module>
    bpl = llvm2bpl(args.infile, args.debug, args.memmod, args.memimpls)
AttributeError: 'Namespace' object has no attribute 'memmod'

If we have a call to a function with just a declaration and no body, such a function will not be declared in the generated bpl file.

e.g. when we encounter an inline assembly call.

One idea would be to have a warning system: generate the Boogie code, and signal to the user that certain code is unsound. This could even be as simple as "WARNING" comments in the generated Boogie code.

smackverify.py chokes on the following program, as float values are assigned to and from the int-value map of (stack-allocated) memory.

#include <smack.h>

void f1(float f);
void f2(float *f);

int main() {
  float f = 0.0;
  f1(f);
  f2(&f);
  return 0;
}

smack-verify.py reports an assertion violation in the following code
-- see examples/failing/struct_init.c introduced by commit eedaf6c

struct a {
  int i;
  int j;
};

int main() {
  struct a x = {0,0};
  __SMACK_assert(x.i == 0);
}

The problem is that we have neither a body nor specification for the memset call which is responsible for initialization; in the generated Boogie code, this appears as

call llvm.memset.p0i8.i64($p1, 0, 8, 4, false);

I suspect the proper fix would be to generate specifications for all memset calls which appear in the generated Boogie program.

M

OUTPUT OF c++ --version

Ubuntu clang version 3.2-1~exp9ubuntu1 (tags/RELEASE_32/final) (based on LLVM 3.2)
Target: i386-pc-linux-gnu
Thread model: posix

USING LLVM : Ubuntu's llvm-3.2-dev package,

./configure --with-llvmsrc=/usr/lib/llvm-3.2/build --with-llvmobj=/usr/lib/llvm-3.2/ --prefix=/home/sergio/smack/

OUTPUT OF make

In file included from BoogieAst.cpp:1:
In file included from /home/sergio/smack/include/BoogieAst.h:5:
In file included from /usr/bin/../lib/gcc/i686-linux-gnu/4.7/../../../../include/c++/4.7/vector:64:
/usr/bin/../lib/gcc/i686-linux-gnu/4.7/../../../../include/c++/4.7/bits/stl_vector.h:1137:52: error: reference to type 'const value_type'
(aka 'smack::Expr _const') could not bind to an lvalue of type 'int'
_M_fill_initialize(static_cast<size_type>(__n), __value);
^~~~~~~
/usr/bin/../lib/gcc/i686-linux-gnu/4.7/../../../../include/c++/4.7/bits/stl_vector.h:393:4: note: in instantiation of function template specialization
'std::vector<smack::Expr *, std::allocator<smack::Expr *> >::_M_initialize_dispatch' requested here
_M_initialize_dispatch(__first, __last, Integral());
^
BoogieAst.cpp:18:23: note: in instantiation of function template specialization 'std::vector<smack::Expr *, std::allocator<smack::Expr *> >::vector'
requested here
vector<Expr> ps(2,NULL);
^
/usr/bin/../lib/gcc/i686-linux-gnu/4.7/../../../../include/c++/4.7/bits/stl_vector.h:1179:59: note: passing argument to parameter '__value' here
_M_fill_initialize(size_type __n, const value_type& __value)
^
In file included from BoogieAst.cpp:1:
/home/sergio/smack/include/BoogieAst.h:55:13: warning: private field 'width' is not used [-Wunused-private-field]
int width;
^
1 warning and 1 error generated.
make[2]: *** [/home/sergio/smack/lib/smack/Debug+Asserts/BoogieAst.o] Error 1
make[2]: Leaving directory /home/sergio/smack/lib/smack' make[1]: *** [all] Error 1 make[1]: Leaving directory/home/sergio/smack/lib'
make: *** [all] Error 1

Here is how to start. First install the latest version of cmake (since LLVM appears not to be working with the one provided by Ubuntu):
wget http://www.cmake.org/files/v2.8/cmake-2.8.12.2-Linux-i386.sh
sudo sh cmake-2.8.12.2-Linux-i386.sh --prefix=/usr/local --exclude-subdir

Then build LLVM like this:
cd llvm/build
cmake -DCMAKE_INSTALL_PREFIX=/home/smack/smack-project/llvm/install ../src

Unfortunately, LLVM 3.3 has a bug and does not compile with cmake. This has been fixed in LLVM 3.4, which SMACK should support soon, at which point this should be implemented as well.

It has something to do with the split memory model I think. I will explore further.

Is there any real reason for this limitation? It seems to be based on the fact that only printf#1 .. printf#5 are declared in the prelude. Maybe we should just have a scheme for generating these declarations? I doubt we'd want to declare every possible (variable argument) library call in the prelude anyways :-)

Problematic example is examples/svcomp/ntdrivers/floppy_unsafe.i.cil.c.
I've been working off the cleaning-alloc branch.

Using twodim, these are the two problematic axioms that get generated:
axiom ($size($obj($pa($ptr(MOUNTDEV_MOUNTED_DEVICE_GUID, 0), 12, 1))) == 8);
axiom ($size($obj($pa($ptr(MOUNTDEV_MOUNTED_DEVICE_GUID, 0), 20, 1))) == 4);

Flat model has the same problems and the axioms there are also wrong, but not inconsistent.

Take a look at the rise4fun folder in the repository. An initial script is already there.

As the following program illustrates, the axioms generated by SMACK for global storage allocation become inconsistent once external storage is declared; SMACK treats such external storage as having size ZERO, and reuses the address of an adjacent storage cell. This leads to two unique constants having the same value, thus inconsistent Boogie axioms.

extern const struct process *procinit[];

int main() {  
  procinit[0] = 0;
  __SMACK_assert(0);
  return 0;
}

This is an example given to us by Akash where the assertion should probably not fail:

int *foo();

int main() {
  int *x = malloc(4);
  int *y = foo();

  *x = 1; *y = 2;

  __SMACK_assert(x != y);
}

Figure out how to build a better infrastructure for regression testing. Look for existing solutions, or write a custom Python script.

This example is failing (see example/failing/struct_assign.c):

#include "smack.h"

struct a {
  int i;
  int j;
};

int main(void) {
  struct a x = {10, 20};
  __SMACK_assert(x.j == 20);
  return 0;
}

The reason is that static initializer for {10, 20} does not get generated.

This is the cause of the problem and the proposed fix works:
http://llvm.org/bugs/show_bug.cgi?id=14301
Hopefully this will make its way into LLVM trunk soon since it is not a SMACK issue.

Regressions containing function pointers are failing, so I guess support for function pointers is currently not implemented.

This omission can be illustrated with the following short example:

#include <stdlib.h>
#include "smack.h"

int g;

int main(void){
  int *x = (int*)malloc(sizeof(int));

  g = 3;
  *x = 5;
  __SMACK_assert(g == 3);
}

The assertion should hold, and yet it currently fails.
The issue is that every access to a global variable is treated as a memory access in LLVM. And SMACK currently does not introduce constraints that all globals should be allocated a priori. Therefore, an assignment to *x can happily overwrite g.

Possible solution: Use "free requires" to ensure that globals are treated as allocated at each procedure entry.

Assertion failed: (isInt(c)), function addStaticInit, file SmackRep.cpp, line 800.

The following example exhibits the problem.

struct a {
int i;
struct a * j;
};

int main(void) {
struct a x = {10, 0};
struct a y = {10, &x};
return 0;
}

Hi, I am trying to check a llvm bitcode file using the command

llvm2bpl.py /hello-world.co

I end up with the file a.bpl with an error printed. I do not have a clue about if it is one problem with my procedure or a problem with smack, if it can be solved or if it would be significantly hard to solve. Do you know what can be going on?

Thank you in advance.

In the following program, SMACK treats each of the two reads of a as a different uninitialized value, and fails the assertion.

int main(void) {
  int a;
  __SMACK_assume(a == 1);
  __SMACK_assert(a == 1);
  return 0;
}

Hi,

when trying to verify file flipping3.bpl (https://gist.github.com/Valpy/8336561) created with smack, using boogie verifier, and I am getting errors: "more than one declaration of function/procedure name". Looking at the flipping.bpl file, you can see that there really os more than one declaration of certain functions (i.e. memcpy.0.0., strcmp). Do you maybe have any idea what is causing this error and how to solve it?

Full report can be found here: https://gist.github.com/Valpy/8336370

P. S. I am using develop version of smack.

Thanks,
Damir

SMACK is not translating static assignments. Consider the following LLVM bitcode which initialises variable "x" with value 3, and "array" as a zero-initialized size 10 array.

@x = global i32 3, align 4
@array = common global [10 x i32] zeroinitializer, align 16

The generated program might want to reflect these assignments at program entry points.

Current scripts have lots of deprecated options and also some hard-coded absolute paths. Clean that up.
Also rename bplgen into llvm2bpl.
Write all scripts in Python.

I ran the build-linux.sh and llvm and smack compile fine, but all the tests in the end give me this output:

Error opening '/home/xxx/smack-project/smack/install/lib/smack.so': /home/xxx/smack-project/smack/install/lib/smack.so: undefined symbol: _ZN4llvm9DebugFlagE
-load request ignored.
opt: Unknown command line argument '-source-loc-syms'. Try: 'opt -help'
opt: Did you mean '-objc-arc-aa'?
opt: Unknown command line argument '-bpl_print'. Try: 'opt -help'
opt: Did you mean '-lint'?
opt: Unknown command line argument '-mem-mod=twodim'. Try: 'opt -help'
opt: Did you mean '-mxgot=twodim'?
opt: Unknown command line argument '-debug-only=bpl'. Try: 'opt -help'
opt: Did you mean '-debug-pass=bpl'?
... (output truncated)
LLVM/SMACK returned exit status 1
two_arrays6_fail (twodim): FAILED

PASSED count: 0
FAILED count: 144

We have an issue with code like this:
_obstack_begin ((&kwset->obstack), 0, 0, (void () ()) xmalloc, (void (*) ()) free);
which gets translated into:
call _obstack_begin($p3, 0, 0, xmalloc, free);
However, first of all free is a keyword in Boogie. Second, free also does not get declared as a unique function pointer constant by SMACK.

The python scripts (llvm2bpl, smackgen, smack-verify) silently fail when there is some problem loading the smack dynamic library -- e.g., when the following happens (on OSX):

Error opening '/Users/mje/lib/smack.dylib': dlopen(/Users/mje/lib/smack.dylib, 9): Symbol not found: __ZN4llvm10DataLayout2IDE

Instead of signaling some problem, these scripts blissfully spit out an empty BPL file. Such errors should be propagated, not ignored.

Currently smack is translating reads of uninitilized variables to reads of an $UNDEF constant. This is not ideal, since to be sound, distinct uninitialized variables need not be equal, i.e., each may have their own value.

Note: I am not exactly sure where LLVM introduces the "UndefValue" which gets translated to $UNDEF (perhaps in some optimization pass?), but the following is what SMACK is currently generating.

Source C code:

int r1;
int r2; 
int result1;
int result2;
result1 = foo(r1);
result2 = foo(r2);

Generated LLVM bitcode:

%1 = load i32* %r1, align 4, !dbg !35
%2 = call i32 @foo(i32 %1), !dbg !35
store i32 %2, i32* %result1, align 4, !dbg !35
%3 = load i32* %r2, align 4, !dbg !36
%4 = call i32 @foo(i32 %3), !dbg !36
store i32 %4, i32* %result2, align 4, !dbg !36

Generated Boogie code:

call $p := foo($UNDEF);
call $p1 := foo($UNDEF);

Precisely supporting bitvector operations is important for some examples. Boogie supports bitvectors, and so we should add support for bitvectors to SMACK as well. The biggest issues is how to define our memory model in that case.

Let's discuss this first before we act on it...

Both Pantazis and I have recently upgraded to OSX Mavericks, and subsequently have independently been running into problems with some of the regression tests. For example, pointers3.c fails during the opt stage, segfaulting while translating foo() (stacktrace at the bottom). We also get the same issue from both the opt plugin and the standalone executable tool (branch smack2tool).

The latest versions seem to still be just fine on an Ubuntu 13.04 machine running an otherwise identical set up.

Have either of you had similar issues?

[dump incoming]

Analyzing function: foo
Inst:   store i32 0, i32* getelementptr inbounds (%struct.point* @p, i32 0, i32 1), align 4, !dbg !27
Inst name:
0  opt                      0x000000010606bbd8 llvm::sys::PrintStackTrace(__sFILE*) + 40
1  opt                      0x000000010606c134 SignalHandler(int) + 564
2  libsystem_platform.dylib 0x00007fff8a9015aa _sigtramp + 26
3  libsystem_platform.dylib 0x000000000000ffff _sigtramp + 1970334319
4  smack.dylib              0x000000010685373a std::__1::__deque_iterator<llvm::User const*, llvm::User const**, llvm::User const*&, llvm::User const***, long, 512l> std::__1::deque<llvm::User const*, std::__1::allocator<llvm::User const*> >::insert<llvm::value_use_iterator<llvm::User const> >(std::__1::__deque_iterator<llvm::User const*, llvm::User const* const*, llvm::User const* const&, llvm::User const** const*, long, 512l>, llvm::value_use_iterator<llvm::User const>, llvm::value_use_iterator<llvm::User const>, std::__1::enable_if<(__is_input_iterator<llvm::value_use_iterator<llvm::User const> >::value) && (!(__is_bidirectional_iterator<llvm::value_use_iterator<llvm::User const> >::value)), void>::type*) + 410
5  smack.dylib              0x0000000106852011 llvm::DSNodeEquivs::getMemberForValue(llvm::Value const*) + 993
6  smack.dylib              0x0000000106718490 smack::DSAAliasAnalysis::alias(llvm::AliasAnalysis::Location const&, llvm::AliasAnalysis::Location const&) + 80
7  smack.dylib              0x00000001067185b7 non-virtual thunk to smack::DSAAliasAnalysis::alias(llvm::AliasAnalysis::Location const&, llvm::AliasAnalysis::Location const&) + 55
8  smack.dylib              0x0000000106759392 llvm::AliasAnalysis::isNoAlias(llvm::AliasAnalysis::Location const&, llvm::AliasAnalysis::Location const&) + 66
9  smack.dylib              0x00000001067563d8 llvm::AliasAnalysis::isNoAlias(llvm::Value const*, llvm::Value const*) + 120
10 smack.dylib              0x000000010674de71 smack::SmackRep::getRegion(llvm::Value const*) + 161
11 smack.dylib              0x000000010674dd7f smack::SmackRep::mem(llvm::Value const*) + 47
12 smack.dylib              0x00000001067268b6 smack::SmackInstGenerator::visitStoreInst(llvm::StoreInst&) + 246
13 smack.dylib              0x0000000106740428 llvm::InstVisitor<smack::SmackInstGenerator, void>::visitStore(llvm::StoreInst&) + 40
14 smack.dylib              0x000000010673fb2b llvm::InstVisitor<smack::SmackInstGenerator, void>::visit(llvm::Instruction&) + 763
15 smack.dylib              0x000000010673f825 void llvm::InstVisitor<smack::SmackInstGenerator, void>::visit<llvm::ilist_iterator<llvm::Instruction> >(llvm::ilist_iterator<llvm::Instruction>, llvm::ilist_iterator<llvm::Instruction>) + 101
16 smack.dylib              0x000000010673f7a2 llvm::InstVisitor<smack::SmackInstGenerator, void>::visit(llvm::BasicBlock&) + 82
17 smack.dylib              0x000000010673eabd llvm::InstVisitor<smack::SmackInstGenerator, void>::visit(llvm::BasicBlock*) + 29
18 smack.dylib              0x000000010673c8e2 smack::SmackModuleGenerator::generateProgram(llvm::Module&, smack::SmackRep*) + 3378
19 smack.dylib              0x000000010674573d smack::SmackModuleGenerator::runOnModule(llvm::Module&) + 109
20 opt                      0x0000000106008675 llvm::MPPassManager::runOnModule(llvm::Module&) + 517
21 opt                      0x0000000106008d0c llvm::PassManagerImpl::run(llvm::Module&) + 540
22 opt                      0x0000000106008efd llvm::PassManager::run(llvm::Module&) + 13
23 opt                      0x000000010551f438 main + 7048
24 libdyld.dylib            0x00007fff88c485fd start + 1
25 libdyld.dylib            0x000000000000000b start + 2000386575
Stack dump:
0.      Program arguments: opt -load=/Users/ethel/work/install/smock/install/lib/smack.dylib -internalize -mem2reg -source-loc-syms -die -lowerswitch -bpl_print -mem-mod=twodim -debug -o=tmp.bc
1.      Running pass 'SMACK generator pass' on module '<stdin>'.

When trying to load smack.so with opt -load build/projects/smack/Debug+Asserts/lib/smack.so [...], I get:

build/projects/smack/Debug+Asserts/lib/smack.so: undefined symbol: _ZN4llvm2cl15GeneralCategoryE
  -load request ignored.

I'm using the smack develop branch, with llvm release_33 and clang release_33

After a successful cas(&p,x,y), SMACK does not ensure that the target pointer's value *p contains the swap value *y. See examples/failing/atomic_cas.c

I have isolated the problem as follows: the target pointer p and swap pointer y are not aliasing for some reason; each is given its own region, so that the assertion *p == *y fails, even when the assertion p == y holds.

My first instinct would be to blame DSA, for not forcing the nodes of p and y to be equivalent.

M

Hi,

i am trying to use smack to generate output boogie file for a LLVM bitcode file (flipping.bc, disassembled file is here: https://gist.github.com/Valpy/8319215 ). After the command "smackgen.py flipping3.bc -o flipping.bpl) I get the following error with the code version 2036610:

LLVM/SMACK encountered an error:
opt: /home/parallels/smack/lib/smack/SmackRep.cpp:800: void smack::SmackRep::addStaticInit(const llvm::Value ): Assertion `isInt(c)' failed.
0 libLLVM-3.3.so 0x00007fa934d6a162 llvm::sys::PrintStackTrace(IO_FILE) + 34
1 libLLVM-3.3.so 0x00007fa934d69db9
2 libpthread.so.0 0x00007fa933adebd0
3 libc.so.6 0x00007fa93343a037 gsignal + 55
4 libc.so.6 0x00007fa93343d698 abort + 328
5 libc.so.6 0x00007fa933432e03
6 libc.so.6 0x00007fa933432eb2
7 smack.so 0x00007fa9329ca897 smack::SmackRep::addStaticInit(llvm::Value const) + 615
8 smack.so 0x00007fa9329d01e8 smack::SmackRepFlatMem::globalDecl(llvm::Value const_) + 56
9 smack.so 0x00007fa9329bb468 smack::SmackModuleGenerator::generateProgram(llvm::Module&, smack::SmackRep*) + 376
10 smack.so 0x00007fa9329c15bd smack::SmackModuleGenerator::runOnModule(llvm::Module&) + 109
11 libLLVM-3.3.so 0x00007fa9346a43ff llvm::MPPassManager::runOnModule(llvm::Module&) + 655
12 libLLVM-3.3.so ... (output truncated)
LLVM/SMACK returned exit status -6

Thank you for your help,

Damir

We should probably prefix all source code names with some symbol other than $. Maybe hash sign (#) would be a good option since it cannot appear in LLVM identifiers.

Same problem as before, this time with another bitcode file. The printed error is the following:

// SMACK-PRELUDE-END

opt: SmackInstVisitor.cpp:159: void smack::SmackInstVisitor::visitCallInst(llvm::CallInst &): Assertion `calledFunction != __null && "Indirect function calls currently not supported"' failed.
0 opt 0x08d3e039
Stack dump:
0. Program arguments: opt -load=/home/sergio/smack/lib/smack.so -internalize -mem2reg -die -lowerswitch -bpl_print -debug-only=bpl -o=tmp.bc

1. Running pass 'SMACK generator pass' on module ''.

When we can determine that pointers point to distinct regions, we should further determine that those pointers cannot be equal. The following example (added as examples/failing/extern_mem2.c by commit db3aa79) demonstrates the problem:

void foo(int*);
int* bar();

int main() {
  int *x = malloc(4);
  int *y = malloc(4);
  int *z;

  foo(y);
  z = bar();

  *x = 1;
  *z = 2;

  __SMACK_assert(x != z);
}

One solution would be to introduce Boogie predicates which determine the region of each pointer, and then axioms that say pointers in separate regions must be different. For instance, in an abridged version of what would be generated from above:

function $R(int) returns (int);
axiom (forall x, y: int :: $R(x) != $R(y) ==> x != y);
// ...
procedure main() {
  call $p1 := $malloc(4);
  assume $R($p1) == 0; // $p1 in region 0
  call $p2 := bar();
  assume $R($p2) == 1; // $p2 in region 1
  assert $p1 != $p2;
}

I vaguely remember that Boogie has an attribute that helps you to achieve this mapping. I'll try to find out more...