Skip to content

port_create_destroy verification hangs in handle_type_is_ptr _ cex mode  #18

@priyasiddharth

Description

@priyasiddharth
/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

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions