goto-analyzer --three-way-merge is not field sensitive

[martin-cs]

$ cat three-way-merge-struct.c
#include <assert.h>

struct s {
  int x;
  int y;
};

struct s global;
int alsoGlobal;

void f00(void) {
  global.x = 0;
}

int main (int argc, char **argv) {
  global.x = 1;
  global.y = 1;
  alsoGlobal = 1;

  f00();

  assert(global.x == 0);
  assert(global.y == 1);
  assert(alsoGlobal == 1);

  global.x = 2;
  global.y = 2;
  alsoGlobal = 2;

  f00();

  assert(global.x == 0);
  assert(global.y == 2);
  assert(alsoGlobal == 2);

  return 0;
}

$ goto-analyzer three-way-merge-struct.c --verify --vsd --three-way-merge --vsd-structs every-field
History not specified, defaulting to --ahistorical
Storage not specified, defaulting to --one-domain-per-history
GOTO-ANALYZER version 5.35.0 (cbmc-5.35.0-101-g06afe802d6) 64-bit x86_64 linux
Parsing /home/martin/tmp/can-delete/three-way-merge-struct.c
Converting
Type-checking three-way-merge-struct
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Selecting abstract domain
Computing abstract states
Performing task
Checking assertions
Function main /home/martin/tmp/can-delete/three-way-merge-struct.c:15
[main.assertion.1] line 22 assertion global.x == 0: SUCCESS
[main.assertion.2] line 23 assertion global.y == 1: SUCCESS
[main.assertion.3] line 24 assertion alsoGlobal == 1: SUCCESS
[main.assertion.4] line 32 assertion global.x == 0: SUCCESS
[main.assertion.5] line 33 assertion global.y == 2: UNKNOWN
[main.assertion.6] line 34 assertion alsoGlobal == 2: SUCCESS

Summary: 5 pass, 0 fail if reachable, 1 unknown

Because three-way-merge iterates over the symbols that have changed rather than the (sub) abstract objects, it is not field sensitive even when a field sensitive abstract object is used. By using a more refined difference that visits the sub-objects within struct and array abstract objects, we can make --three-way-merge field and array element aware.