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

test/dl_context.cpp uses fixed (non-existent) path and segfaults #133

Closed
tautschnig opened this issue Jun 17, 2015 · 1 comment
Closed

Comments

@tautschnig
Copy link

Hi,

The file named here:
https://github.com/Z3Prover/z3/blob/unstable/src/test/dl_context.cpp#L79
might exist on the author's machine, but probably not elsewhere. What's worse, however, is that this causes in invalid memory access that should have been caught somewhere along the following back trace (gdb output):

Testing tr_skip
Eager emptiness checking on

Program received signal SIGSEGV, Segmentation fault.
__GI__IO_fread (buf=0x9bfde9f4, size=1, count=1024, fp=0x0) at iofread.c:41
41 iofread.c: No such file or directory.
(gdb) bt
#0 __GI__IO_fread (buf=0x9bfde9f4, size=1, count=1024, fp=0x0) at iofread.c:41
#1 0x082732db in fread (__stream=, __n=1024, __size=1, __ptr=) at /usr/include/i386-linux-gnu/bits/stdio2.h:295
#2 refill_buffer (start=0, this=) at ../src/muz/fp/datalog_parser.cpp:81
#3 line_reader::get_line (this=0xbfffe640) at ../src/muz/fp/datalog_parser.cpp:160
#4 0x08280577 in get (this=0xbfffe640) at ../src/muz/fp/datalog_parser.cpp:183
#5 next (this=0xbfffe574) at ../src/muz/fp/datalog_parser.cpp:250
#6 set_stream (r=0xbfffe640, s=0x0, this=0xbfffe574) at ../src/muz/fp/datalog_parser.cpp:281
#7 dparser::parse_stream (this=0x9d126574, is=0x0, r=0xbfffe640) at ../src/muz/fp/datalog_parser.cpp:550
#8 0x08281bd2 in dparser::parse_file (this=0x9d126574, filename=0x8f39600 "c:\tvm\src\benchmarks\datalog\t0.datalog") at ../src/muz/fp/datalog_parser.cpp:505
#9 0x081ce4e0 in dl_context_saturate_file (params=..., f=0x8f39600 "c:\tvm\src\benchmarks\datalog\t0.datalog") at ../src/test/dl_context.cpp:65
#10 0x081cea90 in tst_dl_context () at ../src/test/dl_context.cpp:90
#11 0x08054742 in main (argc=2, argv=0xbffff474) at ../src/test/main.cpp:172

Presumably dparser::parse_file should test whether the file has been opened successfully.

Best,
Michael

@tautschnig
Copy link
Author

And here is another use of a non-existent path:
https://github.com/Z3Prover/z3/blob/unstable/src/test/dl_query.cpp#L220
Best,
Michael

NikolajBjorner added a commit that referenced this issue Jun 18, 2015
NikolajBjorner added a commit that referenced this issue Jun 21, 2015
…n violation in poly_simplifier_plugin

Signed-off-by: Nikolaj Bjorner <[email protected]>
wintersteiger pushed a commit to wintersteiger/z3 that referenced this issue Jun 24, 2015
…assertion violation in poly_simplifier_plugin

Signed-off-by: Nikolaj Bjorner <[email protected]>
wintersteiger pushed a commit to wintersteiger/z3 that referenced this issue Jun 24, 2015
wintersteiger pushed a commit to wintersteiger/z3 that referenced this issue Jun 24, 2015
…assertion violation in poly_simplifier_plugin

Signed-off-by: Nikolaj Bjorner <[email protected]>
wintersteiger pushed a commit to wintersteiger/z3 that referenced this issue Jun 24, 2015
wintersteiger pushed a commit to wintersteiger/z3 that referenced this issue Jun 24, 2015
…assertion violation in poly_simplifier_plugin

Signed-off-by: Nikolaj Bjorner <[email protected]>
wintersteiger pushed a commit to wintersteiger/z3 that referenced this issue Jun 24, 2015
wintersteiger pushed a commit to wintersteiger/z3 that referenced this issue Jun 24, 2015
…assertion violation in poly_simplifier_plugin

Signed-off-by: Nikolaj Bjorner <[email protected]>
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

No branches or pull requests

2 participants