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] cannot mention extern arrays without size #708

Open
peterohanley opened this issue Nov 8, 2024 · 0 comments
Open

[CN] cannot mention extern arrays without size #708

peterohanley opened this issue Nov 8, 2024 · 0 comments
Labels

Comments

@peterohanley
Copy link

% cn verify prepro.c
cn: internal error, uncaught exception:
    Failure("the concrete memory model cannot sizeof an array(_,none), from signed int[]")
    Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
    Called from Cerb_frontend__Impl_mem.Concrete.sizeof_ival in file "memory/concrete/impl_mem.ml", line 2465, characters 19-28
    Called from Cn__Memory.size_of_ctype in file "backend/cn/lib/memory.ml", line 58, characters 22-52
    Called from Cn__Resources.range_size in file "backend/cn/lib/resources.ml", line 33, characters 13-36
    Called from Cn__Resources.upper_bound in file "backend/cn/lib/resources.ml", line 37, characters 45-58
    Called from Cn__Check.record_globals.(fun) in file "backend/cn/lib/check.ml", line 2305, characters 24-58
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.run_to_pause in file "backend/cn/lib/typing.ml", line 64, characters 8-21
    Called from Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 165, characters 8-85
    Called from Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 157, characters 6-442
    Re-raised at Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 176, characters 4-69
    Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
    Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44
% gcc -c prepro.c
% cat prepro.c
        extern int a[];

just int a[]; is OK.

@yav yav added the cn label Nov 8, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants