Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CN: Bug - returning struct expression causes a leftover resource #619

Open
dc-mak opened this issue Oct 9, 2024 · 1 comment
Open

CN: Bug - returning struct expression causes a leftover resource #619

dc-mak opened this issue Oct 9, 2024 · 1 comment
Labels
bug Something isn't working cn resource reasoning Related to reasources in specs

Comments

@dc-mak
Copy link
Contributor

dc-mak commented Oct 9, 2024

14:48 ➜  cerberus git:(main) cat tmp.c
#include <stddef.h>

struct MapNode {
    int dummy;
};

struct Map {
    struct MapNode* root;
};

struct Map map_empty()
{
  return (struct Map){ .root = NULL };
}
14:48 ➜  cerberus git:(main) cn verify tmp.c
[1/1]: map_empty -- fail
tmp.c:13:3: error: Left-over unused resource 'Owned<struct MapNode*>(&a_511->root)(NULL)'
  return (struct Map){ .root = NULL };
  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
State file: file:///tmp/state__tmp.c__map_empty.html
14:49 ➜  cerberus git:(main) cn --version
git-0cd00b150 [2024-10-08 08:16:18 +0100]
@dc-mak
Copy link
Contributor Author

dc-mak commented Oct 9, 2024

This however works fine.

   struct Map result = { .root = NULL };
   return result;

@dc-mak dc-mak added bug Something isn't working cn labels Oct 9, 2024
@dc-mak dc-mak changed the title CN: Returning struct expression causes a leftover resource CN: Bug - returning struct expression causes a leftover resource Oct 9, 2024
@dc-mak dc-mak added the resource reasoning Related to reasources in specs label Oct 30, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working cn resource reasoning Related to reasources in specs
Projects
None yet
Development

No branches or pull requests

1 participant