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.