Skip to content

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.

Edited by Quinten Cabo

Merge request reports