V112-002 factor out parsing and printing of composite values

* src/counterexamples/ce_display.adb
(CNT_Element): Removed, replaced by CE_Parsing.Value_Type.
(Component_Loc_Info): Moved to CE_Pretty_Printing.
(Build_Pretty_Line): Simplified, uses
 CE_Pretty_Printing.Print_Value_And_Attributes. Only handle here the
 name of the variable and its order, as well as FOR OF quantified
 variables.
(Build_Variables_Info): Removed, replaced by
 CE_Parsing.Parse_Counterexample_Line.
(Prefix_Elements): Moved to CE_Util.
(Print_CNT_Element_Debug): Removed.
(Refine_Access_Value): Removed, replaced by
 CE_Pretty_Printing.Print_Access_Value.
(Refine_Array_Components): Removed, replaced by
 CE_Pretty_Printing.Print_Array_Value.
(Refine_Record_Components): Removed, replaced by
 CE_Pretty_Printing.Print_Record_Value.
(Refine_Value): Removed, replaced by
 CE_Pretty_Printing.Print_Scalar_Value.
(Refine): Removed, replaced by CE_Pretty_Printing.Print_Value.
(Refine_Attribute): Removed.
(Refine_Iterator_Value): Removed, replaced by Reconstruct_Index_Value.

* src/counterexamples/ce_name_ordered_entities.adb
Removed. Order of variables in CE is handled directly in
CE_Display.Build_Pretty_Line.

* src/counterexamples/ce_parsing.adb
(Value_Type): Type for counterexample values to be shared with CE_RAC.
 It should be close but for things not handled yet in the RAC
 (access values, 'Initialized...). The special case for string values
 is not present.
(Modifier): Flag used when the value given does not correspond to the
 value of the entity at this line but to something else
 ('Old, 'Loop_Entry...).
(Parse_Cnt_Value): Parse the Why3 counterexample value.
(New_Item): Build new counterexample value of appropriate kind.
(Set_Boolean_Flag, Set_Integer_Flag): Read a Why3 counterexample value
 and return it as a boolean/big_integer.
(Parse_Counterexample_Line): Parse a counterexample line and build a
 map of all the values at this line.

* src/counterexamples/ce_pretty_printing.adb
(Value_And_Attributes): Return type of the internal printing functions.
 It contains a string for the value parsed and a list of associations
 pair/value for its attributes.
(Prefix_Names): Prefix all the names in a list of associations
 pair/value by a given prefix.
(Print_Access_Value): Print value of an access type. Designated values
 are printed as allocators, new Ty'(V), instead of the previous
 aggregate like (all => V).
(Print_Array_Value): Print value of an array type in an aggregate
 like syntax. When possible, string values are printed as string
 literals.
(Print_Record_Value): Print value of a record type in an aggregate
 like syntax. Hidden components are prefixed by the name of their
 enclosing type Ty.F => V, where before they had some kind of
 explanation with a location.
(Print_Value): Print a counterexample value as a Value_And_Attributes.
(Print_Value_And_Attributes): Add elements to a counterexample line
 for a counterexample value and its attributes.

* src/counterexamples/ce_utils.adb
(Prefix_Elements, Ultimate_Cursor_Type): Moved from CE_Display.

* tests/K324-014__hidden/test.out
* tests/K324-014__simple/test.out
* tests/K518-029__renaming/test.out
Apparently we used to miss some 'Old modifiers. It is fixed now.

* tests/RB12-009__counterexample_pointer/test.out
* tests/T928-002__at_end_borrow/test.out
Access values are now printed as allocators.

* tests/U730-017__integer32_parsing/test.out
* tests/riposte__array_aggregates/test.out
String values are now printed as string literals.

* tests/NB13-029__discr_bug/test.out
* tests/T212-013__relaxed_init/test.out
* tests/T616-013__initialized/test.out
* tests/U512-015__inlined_functions/test.out
* tests/U520-015__relaxed_init/test.out
* tests/U521-009__access_relaxed_init/test.out
Additional counterexample values which were not printed before. In
particular, additional references to the 'Initialized attribute.

* tests/adacore_u/test.out
Other minor changes.

Change-Id: Ib202252fda0bcceaf3a1109d62fe952bed01cb4e
Depends-On: I5c9d3d47bc842280789d1e5b7e6c172360ddd808