licenses: convert license tags to SPDX

license-tool: missing license headers + .licenseignore [VER-551]

Fix for JIRA VER-443 (scalability of UMM tactic)

The tactic used to establish that a large struct is a umm type doesn't
cope with large number of fields (>= 108 in this case). The translation
used to create a struct containing fields corresponding to all of the
program's addressed globals, but this is actually unnecessary now that
the translation handles these via the locale parameter "symbol_table".

So, the fix is to simply not generate that struct and so not to attempt
to prove the umm-type property of it. Grepping for adglobs in the
verification proof reveals that it isn't used anywhere (as one would
hope), so I'm reasonably confident that this shouldn't cause any wider
regressions. (Fingers crossed.)