8000 [CN-Seq-Test] running seq_test --with-static-check causes duplicate symbol errors · Issue #879 · rems-project/cerberus · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content
8000

[CN-Seq-Test] running seq_test --with-static-check causes duplicate symbol errors #879

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.

Sign up for GitHub

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

Jump to bottom
Open
echoumcp1 opened this issue Feb 18, 2025 · 0 comments
Open

[CN-Seq-Test] running seq_test --with-static-check causes duplicate symbol errors #879

echoumcp1 opened this issue Feb 18, 2025 · 0 comments
Labels
bug Something isn't working cn ui/ux Issue with presentation or user experience

Comments

@echoumcp1
Copy link
Contributor 
ethanchou@Ethans-MacBook-Air-70 tests % cn seq_test runway.pass.c --output-dir=test --num-samples=10 --with-static-hack
runway.pass.c:2:1: warning: Static function 'c_INACTIVE' could not be tested.
Try again with '--with-static-hack'
static int c_INACTIVE() { return 0; }
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
runway.pass.c:4:1: warning: Static function 'c_ACTIVE' could not be tested.
Try again with '--with-static-hack'
static int c_ACTIVE() { return 1; }
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
duplicate symbol '_default_struct_a_1466_record' in:
    /Users/ethanchou/Desktop/research/tests/test/cn.o
    /Users/ethanchou/Desktop/research/tests/test/runway.pass_test.o
duplicate symbol '_cn_map_get_struct_a_1466_record' in:
    /Users/ethanchou/Desktop/research/tests/test/cn.o
    /Users/ethanchou/Desktop/research/tests/test/runway.pass_test.o
duplicate symbol '_cn_map_get_struct_State_cn' in:
    /Users/ethanchou/Desktop/research/tests/test/cn.o
    /Users/ethanchou/Desktop/research/tests/test/runway.pass_test.o
duplicate symbol '_convert_to_struct_State_cn' in:
    /Users/ethanchou/Desktop/research/tests/test/cn.o
    /Users/ethanchou/Desktop/research/tests/test/runway.pass_test.o
duplicate symbol '_depart' in:
    /Users/ethanchou/Desktop/research/tests/test/runway.pass_test.o
    /Users/ethanchou/Desktop/research/tests/test/runway.pass-exec.o
...

Since functions_under_test uses the spec test generation config and not the seq test generation config, the warnings are also triggered despite using --with-static-hack. May have to duplicate the functions_under_test code to use the seq test generation config or add an argument to select the config to use.
@ZippeyKeys12 ZippeyKeys12 added cn bug Something isn't working ui/ux Issue with presentation or user experience labels Feb 18, 2025
@ZippeyKeys12 ZippeyKeys12 changed the title [CN] running seq_test --with-static-check causes duplicate symbol errors [CN-Seq-Test] running seq_test --with-static-check causes duplicate symbol errors Feb 18, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working cn ui/ux Issue with presentation or user experience
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@ZippeyKeys12 @echoumcp1
0