-
Notifications
You must be signed in to change notification settings - Fork 4
Open
Description
/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:]))
Metadata
Metadata
Assignees
Labels
No labels