Skip to content
GitLab
  • Menu
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • sac2c sac2c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 393
    • Issues 393
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 16
    • Merge requests 16
  • Deployments
    • Deployments
    • Releases
  • Wiki
    • Wiki
  • External wiki
    • External wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • sac-group
  • sac2csac2c
  • Merge requests
  • !373

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

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Quinten Cabo requested to merge Quinten/sac2c:improve-type-pattern-errors into develop Apr 01, 2025
  • Overview 1
  • Commits 1
  • Changes 5

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 Apr 04, 2025 by Quinten Cabo
Assignee
Assign to
Reviewer
Request review from
Time tracking
Source branch: improve-type-pattern-errors