SAW stack pointers

ptr.c

#include<stdio.h>

void incptr(int* n){
    *n = *n+1;
}

int* return_out_of_scope(){
    int n=0;
    return &n;
}

int main(){
    int* x = return_out_of_scope();
    incptr(x);
    printf("%d\n",*x);
    return *x; 
}

ptr.saw

m <- llvm_load_module "ptr.bc";

let main_verify= do {
    llvm_execute_func [];
    llvm_return (llvm_term {{1 : [32]}});
};

llvm_verify m "main" [] false main_verify abc;