#147 Ptranal treatment of malloc, etc.

[az bro]

Consider this program:

#include<stdio.h>
#include<stdlib.h>

int main() {
  int *x = malloc(sizeof(int));
  int *y = malloc(sizeof(int));
  x = y;
}

Ptranal produces this output, showing the internal pointer graph:

Computing points-to sets...
tmp(1) -> malloc@3
tmp___0(1) -> malloc@4
x(2) -> malloc@3, malloc@4
y(1) -> malloc@4

This seems reasonable, each allocation site gets its own version of malloc.

However, when you query Ptranal through

Ptranal.resolve_lval (var v)

it conflates all the allocation sites; i.e. resolve_lval returns
a malloc varinfo, the same varinfo for all the sites. The @3, @4, etc.
are forgotten.

I don't know what the right way is to solve this, possibly a change
in the Ptranal interface. For right now, I use the following hack in
Ptranal.ml:

let next_alloc = function
    Lval (Var v, o) ->
      let name = Printf.sprintf "%s@%d" v.vname (fresh_index ()) in
      let vi = Cil.copyVarinfo v v.vname in (* added by CC *)
        A.address (A.make_lvalue false name (Some vi)) (* check *)
  | _ -> raise Bad_return

I.e., I create a new varinfo for malloc, for each call site, each
having a different vid. Presumably, this could break other things
downstream... Another possibility would be to keep the varinfo
vid the same, and change the name to malloc@3, malloc@4, etc.

At the very least, this behavior should be documented.