Make CBMC more fun

[karkhaz]

Summary:

• Add octopus ASCII art logos to CBMC and JBMC frontends
• Change the names of some directories: "goto-instrument" is now
  "goto-inkstrument", "linking" is now "inking", "goto-cc" is now
  "goto-sea-sea", etc.

                                      _________
     _______.         _    _     .___/         \
    /        -_      / \  / \   /  _  _        |
    |    _   _ \     |  \/  |  /  / \/ \       |
    |   / \ / \|     \      /  |  |.||.|       /
    |   |.| |.||      \    /   |  \_/\_/      /
    \_  \_/ \_//       \  /     \  ___      _/
      \      _/         \/       \_\_/     /
      |   \_/                  ___\|      /
     ..____/_..               /.-_/o\____/..
    .. || o\o \~.o.         //~   //..|| \\ ..
   ..  |/ .||    \\..     //     || ..|| ||  ..
   .. //o .o\\    || .. //      // .. // ||   .
  ..  ||  .. \o   \\  //.     //  ..  || ||   ..
..   o//  ..  \\   ^\// ..  //    .  |/ .\|    ..
.    //  ..    ||   /\    .//    .. //  . \\   ..
.   |/  ..     \|  //\|   ||     ../|  .. ||   ..
    o  ..       o  l  o  //..     .|\ ..  \\  ..
      ..                |/  ..     |/ ..   \| ..
                        o    .     o        o

           ______________  ________
          /  __ | ___ |  \/  /  __ \
          | /  \| |_/ | .  . | /  \/
          | |   | ___ | |\/| | |
          | \__/| |_/ | |  | | \__/\
           \____\____/\_|  |_/\____/

Logo information:

The octopus on the left is the "model-checking octopus," and the one on
the right is the "path exploration octopus". Their lovemaking symbolises
the retrofitting of path-exploration functionality to CBMC in #1641.

Rationale:

We're hoping to boost CBMC's uptake and retention amongst customers by adding a fun logo. The "mating octopi" logo was crafted during a several-month long rebranding and outreach effort. We found that customers form positive associations with tech brands that feature cute animals as opposed to fruits or rectangles. Members of the verification community have responded warmly to this proposed logo; below are a selection of quotes:

This is a charming logo, I hope to see it when using CBMC to verify
my latest sorting algorithm! Just to think, if only I had devised
such a magnificent logo for my process calculus in the 80s, it would
not have been usurped by Robin's bald-faced ripoff.
-- Tony

I like the idea, but don't eight-legged animals have a very large
footprint? The logo is also off-centre, adding a proper frame would
help here. Finally, the octopuses appear to be hopelessly tangled up
and ought to be separated. Fortunately, I came up with a neat trick
back in 2001 that could help you with all of these problems...
-- Peter

You're adding a _logo_ to a _verification tool_? goto hell.
-- Edsgar

[tautschnig]

I think we need to make sure this gets merged today.

[mgudemann]

please fix ccache /usr/bin/g++-5 -D_GLIBCXX_DEBUG -c -MMD -MP -std=c++11 -O2 -DHAVE_MINISAT2 -Wall -pedantic -Werror -I .. -o ansi_c_language.o ansi_c_language.cpp ansi_c_language.cpp:18:27: fatal error: inking/inking.h: No such file or directory compilation terminated.
else looks fun to me, @tautschnig is right, needs to go in today

[peterschrammel]

I think @thk123 needs to create TG bump first.

[smowton]

Clearly we need to fix the linter to enforce all available nautical puns

[karkhaz]

I'm closing this PR as our users found goto-sea-sea much more cumbersome to type. We'll continue working on this and hopefully have an improved version next year.