Skip to content

Commit

Permalink
Added another failing example.
Browse files Browse the repository at this point in the history
* pointers to separate regions should be unequal.
  • Loading branch information
michael-emmi committed Mar 18, 2014
1 parent eedaf6c commit db3aa79
Showing 1 changed file with 19 additions and 0 deletions.
19 changes: 19 additions & 0 deletions examples/failing/extern_mem2.c
@@ -0,0 +1,19 @@
#include <stdlib.h>
#include <smack.h>

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);
}

0 comments on commit db3aa79

Please sign in to comment.