Extern symbols linking

[rafaelsamenezes]

Note: This is an incorrect approach for this! I am opening this as a PR so I can properly fix at ucode branch. Right now the PR is adding external symbols later on the flow.

@mikhailramalho any suggestions on how to implement this correctly?

This intends to fix linking issues from external symbols.

// extern.h
extern int arr[];

// extern.c
#include "extern.h"
int arr[4];

// main.c
#include "extern.h"
int main() {
  int a  = arr[3]; // ESBMC throws out-of-bounds
  return 0;
} 

[mikhailramalho]

Merging the IR has been a pain for a long time :(

The best solution IMHO is to use clang to merge to ASTs before we convert them to our internal representation; this will require a lot of work tho.

The more approachable solution would be to update c_link to properly handle these cases. It shouldn't be too hard given that CBMC already does it.

[rafaelsamenezes]

Closing since #881 supersedes this.