[pointer analysis] Assertion `is_struct_type(type) || is_union_type(type)' failed.

[lucasccordeiro]

$esbmc alglin1.c --function det2 --incremental-bmc

esbmc: /home/lucas/ESBMC_Project/esbmc/src/pointer-analysis/value_set.cpp:1439: expr2tc value_sett::make_member(const expr2tc&, const irep_idt&): Assertion `is_struct_type(type) || is_union_type(type)' failed.
Aborted

test.zip

[fbrausse]

This looks related to variadic functions on 64-bit (#584):

(gdb) p type->dump()
pointer
* subtype : signedbv
    * width : 32

and

(gdb) up
#6  0x00005555558333a2 in value_sett::make_member (this=0x555564a49270, src=..., component_name=...)
    at ../src/pointer-analysis/value_set.cpp:1475
1475	    return make_member(to_typecast2t(src).from, component_name);
(gdb) p src->dump()
typecast
* from : address_of
    * pointer_obj : symbol
        * name : c:pariinl.h@31617@F@gerepileall@n
        * renamelev : Level 1
        * level1_num : 1
        * level2_num : 0
        * thread_num : 0
        * node_num : 0
        * type : signedbv
          * width : 32
    * type : pointer
      * subtype : signedbv
          * width : 32
* rounding_mode : constant_int
    * value : 0
    * type : signedbv
      * width : 32
* type : struct
  * members : 
    0: unsignedbv
      * width : 32
    1: unsignedbv
      * width : 32
    2: pointer
      * subtype : empty
    3: pointer
      * subtype : empty

  * member_names : 
    0: gp_offset
    1: fp_offset
    2: overflow_arg_area
    3: reg_save_area

  * member_pretty_names : 
    0: gp_offset
    1: fp_offset
    2: overflow_arg_area
    3: reg_save_area

  * typename : struct __va_list_tag
  * packed : false

Indeed, running with --32 works and gives VERIFICATION FAILED.

[intrigus-lgtm]

"Fixed" between v7.6 and v7.6.1 to crash with a sigsegv instead of assertion. Actually fixed between v7.6.1 and v7.8 so likely by https://github.com/esbmc/esbmc/pull/2207.