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

NULL pointer dereference on verbosity command #5448

Closed
rainoftime opened this issue Nov 15, 2020 · 1 comment · Fixed by #5512
Closed

NULL pointer dereference on verbosity command #5448

rainoftime opened this issue Nov 15, 2020 · 1 comment · Fixed by #5512
Assignees

Comments

@rainoftime
Copy link

rainoftime commented Nov 15, 2020

Hi, for the following formula, CVC4 a71274b

(set-logic NIA)
(synth-inv InvF ((x1 Int)))
(check-synth)

$ /cvc4 x.sl  -vvv
Invoking: (set-option :incremental false)

Invoking: (set-logic NIA)

CVC4 suffered a segfault in DEBUG mode.
Offending address is 0xe0
Looks like a NULL pointer was dereferenced.
Invoking: Aborted
@rainoftime rainoftime changed the title NULL pointer dereference with verbosity commad NULL pointer dereference on verbosity command Nov 15, 2020
@ajreynol
Copy link
Member

Stack trace:

Program received signal SIGSEGV, Segmentation fault.
0x00000000004241a3 in CVC4::api::Grammar::resolve (this=0x0) at /space/ajreynol/cvc4-ajr/src/api/cvc4cpp.cpp:2878
2878	/space/ajreynol/cvc4-ajr/src/api/cvc4cpp.cpp: No such file or directory.
(gdb) bt
#0  0x00000000004241a3 in CVC4::api::Grammar::resolve (this=0x0) at /space/ajreynol/cvc4-ajr/src/api/cvc4cpp.cpp:2878
#1  0x00000000004d3f14 in CVC4::SynthFunCommand::toStream (this=0x254b4c0, out=..., toDepth=-1, dag=1, language=CVC4::language::output::LANG_SYGUS_V2)
    at /space/ajreynol/cvc4-ajr/src/smt/command.cpp:660
#2  0x00000000004d1111 in CVC4::operator<< (out=..., c=...) at /space/ajreynol/cvc4-ajr/src/smt/command.cpp:55
#3  0x000000000040c35f in CVC4::main::CommandExecutor::doCommand (this=0x2520f20, cmd=0x254b4c0) at /space/ajreynol/cvc4-ajr/src/main/command_executor.cpp:96
#4  0x0000000000407896 in CVC4::main::CommandExecutor::doCommand (this=0x2520f20, cmd=...) at /space/ajreynol/cvc4-ajr/src/./main/command_executor.h:76
#5  0x000000000040657f in runCvc4 (argc=3, argv=0x7fffffffdf28, opts=...) at /space/ajreynol/cvc4-ajr/src/main/driver_unified.cpp:448
#6  0x000000000040bc00 in main (argc=3, argv=0x7fffffffdf28) at /space/ajreynol/cvc4-ajr/src/main/main.cpp:54
(gdb) quit
A debugging session is active.

	Inferior 1 [process 15801] will be killed.

ajreynol pushed a commit that referenced this issue Dec 8, 2020
This PR fixes #5448. SynthFunCommand::toStream used to call d_grammar->resolve even when d_grammar is a nullptr. This PR fixes the issue and modifies the signature of Printer::toStreamCmdSynthFun to make it clear that grammar is an optional argument.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants