Do not error on undef extern linker symbols

goto-cc currently parses the linker script given by the -T flag to find addresses for variables that are extern-declared in C files but not given a definition. This is because some variables are defined in the linker script, not in C code, and reading these definitions from the linker script is necessary to verify the C program.

Prior to this commit, goto-cc would error out if some extern-defined variables remained undefined even after reading the linker script. There is actually a valid use case for having undefined symbols even after linking, see this (search for "Undefined symbol to cause link failure"):

    https://lore.kernel.org/all/[email protected]/T/

This commit turns the error into a warning and synthesizes a null pointer for such symbols.

Author: karkhaz

src/goto-cc/linker_script_merge.cpp

@@ -728,16 +728,19 @@ int linker_script_merget::get_linker_script_data(
 
 int linker_script_merget::goto_and_object_mismatch(
     const std::list<irep_idt> &linker_defined_symbols,
-    const linker_valuest &linker_values)
+    linker_valuest &linker_values)
 {
   int fail=0;
   for(const auto &sym : linker_defined_symbols)
     if(linker_values.find(sym)==linker_values.end())
     {
-      fail=1;
-      log.error() << "Variable '" << sym
+      log.warning() << "Variable '" << sym
                   << "' was declared extern but never given "
                   << "a value, even in a linker script" << messaget::eom;
+
+      null_pointer_exprt null_pointer(pointer_type(char_type()));
+      symbol_exprt null_sym(sym, pointer_type(char_type()));
+      linker_values.emplace(sym, std::make_pair(null_sym, null_pointer));
     }
 
   for(const auto &pair : linker_values)

src/goto-cc/linker_script_merge.h

@@ -198,7 +198,7 @@ class linker_script_merget
   ///   everything is OK.
   int goto_and_object_mismatch(
       const std::list<irep_idt> &linker_defined_symbols,
-      const linker_valuest &linker_values);
+      linker_valuest &linker_values);
 
   /// \brief Validate output of the `scripts/ls_parse.py` tool
   int linker_data_is_malformed(const jsont &data) const;