Doxygen for test gen support

[reuk]

Reformats the documentation in test-gen-support to be doxygen-compatible. Similar to #869, but targets test-gen-support instead of master.

[reuk]

Before this gets merged, I need to add the small script update from #1005. This won't affect the docs at all, just the conversion script.

[reuk]

This has now been updated with the fix from yesterday evening.

[allredj]

We might want to think for a bit before we introduce a new format that will haunt us until the end of time.

Personally, I find:

-/*******************************************************************\
 -
 -Function: string_constraint_generatort::add_default_axioms
 -
 -  Inputs:
 -    s - a string expression
 -
 - Outputs: a string expression that is linked to the argument through
 -          axioms that are added to the list
 -
 - Purpose: adds standard axioms about the length of the string and
 -          its content:
 -          * its length should be positive
 -          * it should not exceed max_string_length
 -          * if force_printable_characters is true then all characters
 -            should belong to the range of ASCII characters between ' ' and '~'
 -
 -
 \*******************************************************************/

to be much more readable than:

 +/// adds standard axioms about the length of the string and its content: * its
 +/// length should be positive * it should not exceed max_string_length * if
 +/// force_printable_characters is true then all characters should belong to the
 +/// range of ASCII characters between ' ' and '~'
 +/// \param s: a string expression
 +/// \return a string expression that is linked to the argument through axioms
 +///   that are added to the list

It's not a problem with doxygen itself, but rather of the proposed typesetting. Although I like the compactness, will we have any freedom in arranging how our documentation looks in the code? I usually spend much more time in the code than on the doxygen-generated pages, so I believe that how the documentation looks in the code is still important. Or are there IDE tweaks I don't know about? What are your thoughts?

BTW, the python script looks good. I have nothing to say about that.

[reuk]

I agree, but I also think that this is a bit of a corner-case example - the conversion script can handle custom formatting in Purpose blocks, but only if there's an empty line between the first paragraph and the block with the fancy formatting. In this particular case, the doxygen output should probably be fixed-up a little so that it looks more like this:

/// Adds standard axioms about the length of the string and its content:
/// * its length should be positive
/// * it should not exceed max_string_length
/// * if force_printable_characters is true then all characters should belong to the
///   range of ASCII characters between ' ' and '~'
/// \param s: a string expression
/// \return a string expression that is linked to the argument through axioms
///   that are added to the list

You could even add an empty line (still with /// at the beginning) after the bullet list...
Because the existing comments don't have a consistent format, it's difficult to write a script which can convert all possible doc comments in a pretty, readable way. Therefore, I would say that

• it's fine/encouraged to fix up formatting in illegible doxygen comments
• having readable docs should be prioritised over consistency. So, if a comment looks good in the code and in doxygen, and doesn't diverge too much from the 'normal' style, it should be allowed to pass peer review

[allredj]

OK then! Thanks for the great job!