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

port_create_destroy verification hangs in handle_type_is_ptr _ cex mode #18

Open
priyasiddharth opened this issue Aug 8, 2022 · 0 comments

Comments

@priyasiddharth
Copy link
Collaborator

/tmp/verifyTrusty/storage_ipc_port_create_destroy.ir.fat.pp.ms.o.ul.cut.o.bc --horn-unify-assumes=false
--horn-gsa=false --horn-vcgen-use-ite --horn-vcgen-only-dataflow=false --horn-bmc-coi=false --sea-opsem-a
llocator=static --horn-explicit-sp0=false --horn-bv2-lambdas=false --horn-bv2-simplify=true --horn-bv2-ex
tra-widemem --horn-stats=true --horn-array-sym-memcpy-unroll-count=10 --horn-bmc-hexdump=true --horn-bmc-
logic=QF_ABV
Warning: not lowering an initializer for a global struct:  port_ctx
Sea-Dsa type aware!
Omnipotent char: omni_i8*
Info: pointer size: 8, word size: 8
Info: Trackable memory is not present
Warning: Skipping global variable marked by llvm.metadata section: @llvm.used
Functions:
0x00000008048000 @handle_port.addr
0x00000008048008 @sea_channel_connect.addr
Globals:
0x00000008048010 @msg_buf
0x00000008048018 @.str.39
0x00000008048040 @port_ctx
0x00000008048068 @g_ptr0
!3 Alloca of 1 bytes:   %msg_buf_size = alloca i1, !sea.dsa.allocsite !633
!3 Alloca of 8 bytes:   %g_ptr0_size = alloca i64, !sea.dsa.allocsite !182
!3 Alloca of 40 bytes:   %malloc.i1 = alloca %struct._handleState, align 16, !sea.dsa.allocsite !291
!3 Alloca of 4096 bytes:   %malloc14.i2 = alloca [4096 x i8], align 16, !sea.dsa.allocsite !783
^CTraceback (most recent call last):
  File "/home/siddharth/seahorn/seahorn/build-dbg/run/bin/sea", line 73, in <module>
    sys.exit (main (sys.argv[1:]))
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

1 participant