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] Crash when logging SMT output with --solver-logging #874

Open
septract opened this issue Feb 15, 2025 · 0 comments
Open

[CN] Crash when logging SMT output with --solver-logging #874

septract opened this issue Feb 15, 2025 · 0 comments
Assignees
Labels
bug Something isn't working cn

Comments

@septract
Copy link
Collaborator

CN crashes with too many open files when logging SMT output using --solver-logging.

Replication

Test file open_files_minimized.c (generated from @cp526's pagetable code by creduce):

enum a { b, c, d };
long e() {}
long f() { long g; }
void h(enum a i, long j) {
  _Bool device = i & d;
  int k = device ? 4 : 0, l, ap = 0 ? 1 : 3;
  long attr = 0 << 0 << 0 >> 0 >> 0;
  if (i & c)
    ;
  attr |= 0;
}

Output:

$ cn verify --solver-logging=blah open_files_minimized.c
cn verify --solver-logging=blah open_files_minimized.c
[1/3]: e -- fail
[2/3]: f -- fail
[3/3]: h -- pass
open_files_minimized.c:2:1: error: Undefined behaviour
long e() {}
~~~~~^~~~~~
the value of a non-void function that ended without a return statement is used
State file: file:///var/folders/sl/2lpz4lb10ylbnbzqplt1bjj00000gp/T/state__open_files_minimized.c__e.html
cn: internal error, uncaught exception:
    Sys_error("/var/folders/sl/2lpz4lb10ylbnbzqplt1bjj00000gp/T/state__open_files_minimized.c__f.html: Too many open files")
    Raised by primitive operation at Stdlib.open_out_gen in file "stdlib.ml", line 329, characters 29-55
    Called from Stdlib.open_out in file "stdlib.ml" (inlined), line 334, characters 2-74
    Called from Cn__Report.make in file "backend/cn/lib/report.ml", line 814, characters 11-28
    Called from Cn__TypeErrors.report_pretty in file "backend/cn/lib/typeErrors.ml", line 638, characters 17-72
    Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
    Called from Dune__exe__Main.verify.(fun).check in file "backend/cn/bin/main.ml", line 339, characters 10-242
    Called from Cn__Typing.run_from_pause in file "backend/cn/lib/typing.ml", line 68, characters 50-55
    Called from Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 164, characters 6-573
    Re-raised at Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 186, 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

CN version: git-ba4a38312 [2025-02-13 16:43:44 -0500]

For some reason, this bug does not occur when I call CN through the embedded shell in VS Code. This seems totally bizarre to me - I have no idea what's going on.

@septract septract added bug Something isn't working cn labels Feb 15, 2025
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
Projects
None yet
Development

No branches or pull requests

2 participants