Skip to content

goto-cc crashes on softfloat code using __int128 #5103

@andreast271

Description

@andreast271

CBMC version: gcc (goto-cc 5.12 (crest.merged-48-gabe78fc77-dirty)) 7.4.0
Operating system: 4.15.0-45-generic x86_64 GNU/Linux
Exact command line resulting in the issue: goto-cc sf.c
What behaviour did you expect: no crash
What happened instead: invariant failure

The following is a reduced version of the softfloat code causing the crash:
file sf.c:

void softfloat_mul128To256M(unsigned a)
{
  unsigned __int128 z;
  z = (unsigned __int128) a;
  z += (a < 1);
}

command: goto-cc sf.c

output:

--- begin invariant violation report ---
Invariant check failed
File: ../util/std_types.h:1091 function: to_bitvector_type
Condition: can_cast_type<bitvector_typet>(type)
Reason: Precondition
...

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions