Compilers do not bake the final semantics of a source file into the resulting object file: the behaviour of an object file can subsequently be changed by the linker when it links several objects into an executable. In particular, the linker can define symbols and other data that the correctness of the program depends on, but which are totally absent from the source code itself. This presents a challenge for verification tools, whose knowledge of the program's behaviour is derived entirely from the program's source code. In this talk, we'll review the operation of a linker; describe how the use of linker scripts can frustrate attempts to verify program correctness; and present a semantics for interpreting linker scripts, from the perspective of a static analysis tool, to overcome these difficulties. We have implemented this interpretation in the CBMC bug-finding tool, and used it to prove the correctness of a non-trivial low-level program.