[Condorcet] Add annotations to check code with SPARK GPL 2014

* Several functions are defined out of SPARK. Should be fixed later.
[Condorcet] Regenerate test harness, it changed some test ids
gitignore GNAT GPL 2014 generated files