Add exactly which pre- or post-condition failed in type pattern error message

This mr adds exactly which pre- or post-condition failed in type pattern error message instead of just which function failed.

Example

This code:

int bar(int x) | _ge_SxS_(x, 2), _le_SxS_(x, 10){
    return x;
}

int main() {
    a = _hideValue_SxA_(1, [15]);
    b = _sel_VxA_([0], a);
    ba = bar(b);
    return 0;
}

Would previously give this error message (when compiling with -check p):

*** Type pattern pre-condition of bar failedType pattern pre-condition of bar failed

But after merging this it will give:

Type pattern pre-condition _le_SxS_(x, 10) of bar failed

Printing expressions

To achieve this I added a new function called CVexpr2String to convert.c and convert.h which converts any expression node into a string. This also required modifying print.c a bit because by default things which are printed when global.outfile is not NULL using the PrintTRAVdo function get these large /****************/ around them. These look ugly and out of place in the error messages. Removing these section dividers (is what I called the lines) broke the test-assoc-law test. I added a printTRAVdo_section_dividers boolean to the INFO struct of the print.c traversal. This boolean is accessible with the INFO_PRINT_SECTION_DIVIDERS macro. By default (in MakeInfo) this boolean is set to TRUE to keep the old behavior as the default. I added PRTdoPrintNodeWithoutSectionDividers which is exactly like PRTdoPrintNode, but it sets printTRAVdo_section_dividers to false in the info struct before calling PrintTRAVdo.

Finally, this PRTdoPrintNodeWithoutSectionDividers is what is used in CVexpr2String.

MakeConditionalGuards

The error message which is thrown when a predicate type pattern pre- or post-condition fails is generated statically in type_pattern_guard.c in MakeConditionalGuards. This is nice because we just have the predicate condition. We can turn the predicate expression into a string using the new CVexpr2String and put it in the error message.

I decided to remove the leading comma if it was there in the type pattern boolean expression. All predicates besides the last one have this leading comma. As far as I know there is never a valid expression which ends in a comma. I think it is prettier to remove it.

I think that there was also a mistake in the original MakeConditionalGuards. The mistake was that the string buffer of the previous condition was not cleared. This means that if condition 3 of a function call failed it would also print that condition 1 and 2 failed. This is what the SBUFflush at the end of the MakeConditionGuards while loop is for.

added error-messages type-pattern labels

It would be even nicer if the error message could be:

Type pattern pre-condition _le_SxS_(x, 10) of bar failed when bar was called from main.

We only really need to go one level up in giving the programmer information about the call trace because in theory if everyone always annotates all the constraints on all the functions it will only go wrong once at bar. The execution would not have gotten to the function that called bar if all the predicates would not hold of that function.

I will branch of this branch to see if I can make this happen.

approved this merge request

changed the description