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 401
    • Issues 401
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 13
    • Merge requests 13
  • 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
  • !395

Added Return Value Patterns

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged David Logtenberg requested to merge DavidL/sac2c:david/return-pattern into develop May 09, 2025
  • Overview 9
  • Commits 14
  • Changes 12

Added a function to fit identifiers on the return values of functions. For example,

int[n]{r} foo(int[n] x)
  | _all_V_(_gt_VxS_(r, 0))
{
    return x;
}

is now valid, with the return value in the postcondition being mapped to r.

Edited May 15, 2025 by Jordy Aaldering
Assignee
Assign to
Reviewer
Request review from
Time tracking
Source branch: david/return-pattern