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

[BUG] CN crashes if spec arg list does not match function #102

Open
3 of 4 tasks
peterohanley opened this issue Jun 18, 2024 · 0 comments
Open
3 of 4 tasks

[BUG] CN crashes if spec arg list does not match function #102

peterohanley opened this issue Jun 18, 2024 · 0 comments
Labels
bug Something isn't working CN Issues related to the CN tool
Milestone

Comments

@peterohanley
Copy link
Collaborator

Summary

Rather than print location information CN crashes on this input.

Bug

void f(char *p);
/*@ spec f(pointer p, i32 a);
    requires true;
    ensures true;
@*/
% cn arg_mismatch.c                           
cn: internal error, uncaught exception:
    Invalid_argument("List.combine")
    Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
    Called from Stdlib__List.combine in file "list.ml", line 305, characters 36-49
    Called from Dune__exe__Core_to_mucore.normalise_fun_map_decl in file "backend/cn/core_to_mucore.ml", line 1328, characters 19-74
...

Acceptance Criteria

Print a normal syntax error with location information.

Do

  • assign issue to a Milestone
  • define acceptance criteria
  • add appropriate labels
  • Check the list lengths before calling list combine
@peterohanley peterohanley added bug Something isn't working CN Issues related to the CN tool labels Jun 18, 2024
@peterohanley peterohanley added this to the MVP 2 milestone Jun 18, 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 Issues related to the CN tool
Projects
None yet
Development

No branches or pull requests

1 participant