Memory regions in Boogie using Data Structure Analysis

[l-kent]

Implements #249

• Adds a --memory-regions dsa option to insert regions based on the Data Structure Analysis results into the Boogie output
• The existing version of memory region insertion can now be used by using --memory-regions mra
• Fixes issue with invalid characters appearing in DSA .dot file output
• External functions/objects listed in the symbol table are now handled correctly in the DSA, with the pointers being correctly treated as having size 8, renamed to indicate that they are pointing to the external function, and they now point to a new ExternalLocation which represents the abstract external function or object
• Adds DSAMemoryRegionSystemTestsBAP and DSAMemoryRegionSystemTestsGTIRB test suites which run all SystemTests with the --memory-regions dsa option set

The DSA-based memory regions are currently able to handle all existing test cases successfully, though it likely does not handle anything involving overlapping accesses successfully yet since the DSA implementation there is not yet finished. It tracks the memory regions by creating a new Map, accessIndexToSlice, which maps from MemoryLoads and MemoryStores to Slices representing the indices of the accesses. This mapping is used as the basis for regions, with distinct cells representing distinct memory regions.

[sadrabt]

Is size necessary? i don't think it is used by DSA MRA region injector? I think it also makes sense to check if the size is covered by the cell. But I assume this wouldn't hold for examples with globals with disjoint fields (cells) because the size passed as a parameter is the whole global region's size. However, maybe this is not necessary until we have better field-sensitivity implemented

[sadrabt]

The rest looks good to me

[sadrabt]

DSA-Regions extra Constraints #280