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-Exec] EOF error when NULL macro is used #654

Open
dc-mak opened this issue Oct 25, 2024 · 4 comments
Open

[CN-Exec] EOF error when NULL macro is used #654

dc-mak opened this issue Oct 25, 2024 · 4 comments
Assignees
Labels
bug Something isn't working CN spec testing cn CN-exec Related to CN executable spec generation, called using `cn instrument`

Comments

@dc-mak
Copy link
Contributor

dc-mak commented Oct 25, 2024

#ifndef NULL           
#define NULL ((void*)0)
#endif                 
                       
int main()             
{                      
    int *p = NULL;     
}                      
15:34 ➜  VST git:(VST) ✗ /home/dhruv/.opam/4.14.1/lib/cn/runtime/libexec/cn-runtime-single-file.sh -o tmp.c
cn: internal error, uncaught exception:
    End_of_file
    Raised at Stdlib.unsafe_really_input in file "stdlib.ml", line 429, characters 9-26
    Called from Stdlib.really_input_string in file "stdlib.ml", line 440, characters 2-25
    Called from Cn__Source_injection.move_to.aux in file "backend/cn/lib/source_injection.ml", line 122, characters 10-49
    Called from Cn__Source_injection.inject in file "backend/cn/lib/source_injection.ml", line 174, characters 14-48
    Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
    Called from Cn__Source_injection.inject_all in file "backend/cn/lib/source_injection.ml", line 260, characters 11-72
    Called from Cn__Source_injection.output_injections.(fun) in file "backend/cn/lib/source_injection.ml", line 419, characters 13-49
    Called from Cerb_colour.without_colour in file "util/cerb_colour.ml", line 40, characters 10-13
    Called from Cn__Executable_spec.main.(fun) in file "backend/cn/lib/executable_spec.ml", line 393, characters 7-229
    Called from Dune__exe__Main.generate_executable_specs.(fun) in file "backend/cn/bin/main.ml", line 408, characters 10-272
    Called from Cerb_colour.without_colour in file "util/cerb_colour.ml", line 40, characters 10-13
    Called from Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 169, characters 6-443
    Re-raised at Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 188, 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
Failed to generate C files from CN-annotatated source.
@dc-mak dc-mak added cn bug Something isn't working labels Oct 25, 2024
@yav
Copy link
Collaborator

yav commented Nov 7, 2024

This happens with other macros as well. Seems to be related to the length of the definition, I have an example where:

#define KEY int     // Works fine
#define VALUE long  // Works 

However, defining KEY like this causes the error above:

#define KEY unsigned int 

@dc-mak
Copy link
Contributor Author

dc-mak commented Nov 21, 2024

Duplicate of #393

@dc-mak dc-mak marked this as a duplicate of #393 Nov 21, 2024
@dc-mak dc-mak closed this as completed Nov 21, 2024
@dc-mak
Copy link
Contributor Author

dc-mak commented Nov 21, 2024

Work-around is to preprocess file before instrumenting the code, which is what we do in the CI.

@dc-mak
Copy link
Contributor Author

dc-mak commented Nov 21, 2024

Actually this the single file script should be preprocessing so maybe this needs to stay open

@dc-mak dc-mak reopened this Nov 21, 2024
@rbanerjee20 rbanerjee20 added the CN-exec Related to CN executable spec generation, called using `cn instrument` label Nov 26, 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 spec testing cn CN-exec Related to CN executable spec generation, called using `cn instrument`
Projects
None yet
Development

No branches or pull requests

3 participants