Locations for accesses in guards cover entire statement

[vesalvojdani]

When accesses occur in loop guards, the access location covers the entire body of the statement. It makes it very unreadable inside GobPie for real-world examples like this:

#include <pthread.h>
#include <stdio.h>

int myglobal;

void *t_fun(void *arg) {
  if (myglobal > 0) {
    printf("Stupid!");
    printf("Stupid!");
    printf("Stupid!");
    printf("Stupid!");
    printf("Stupid!");
    printf("Stupid!");
  }
  return NULL;
}

int main(void) {
  pthread_t id;
  pthread_create(&id, NULL, t_fun, NULL);
  myglobal=myglobal+1;
  pthread_join (id, NULL);
  return 0;
}

I tried a fix in 076660b, but it's not clear if that causes issues with our use of locations for other things. Are there cases when we'd want the location to cover the entire statement?

[sim642]

There must be some other reason for this happening on interactive, because on master the same code correctly returns only the expression location:

[Warning][Race] Memory location myglobal@foo.c:4:5-4:13 (race with conf. 110):
  read with [mhp:{tid=[main, t_fun@foo.c:20:3-20:40]},
           thread:[main, t_fun@foo.c:20:3-20:40]] (conf. 110) (foo.c:7:7-7:19)
  write with [mhp:{tid=[main]; created={[main, t_fun@foo.c:20:3-20:40]}}, thread:[main]] (conf. 110) (foo.c:21:3-21:22)

[vesalvojdani]

I see... but I presume you confirmed it is different on that branch where that great CilFacade0 layer is doing its thing. :)

[sim642]

I suspect the issue is #533, according to which accesses and their warnings are associated with CFG nodes on interactive. But I think the default current_loc on master uses the location from CFG edge instead.

Having these statements in the CFG nodes and constraint unknowns is an endless source of confusion because statements (and conditional guards) correspond to edges, not nodes. Nodes cannot uniquely identify the corresponding transfer function locations at branch or join points, depending on which is incorrectly used during a transfer function.