Skip to content

Imprecise cast overflows in sv-benchmarks #1586

Open
@sim642

Description

@sim642

Regarding the question whether casts are overflows in SV-COMP, I ran Goblint both ways and inspected the verdict differences. There are a bunch of tasks where it seems that we are just rather imprecise if casts were to be counted as overflows:

  • Juliet_Test/CWE190_Integer_Overflow__int_connect_socket_*_good (152 tasks): implicit cast ssize_t (long int) -> int on LP64, Goblint imprecise: recv doesn't return bigger than len argument
  • Juliet_Test/CWE190_Integer_Overflow__int_listen_socket_*_good (152 tasks): implicit cast ssize_t (long int) -> int on LP64, Goblint imprecise: recv doesn't return bigger than len argument
  • Juliet_Test/CWE190_Integer_Underflow__int_{connect,listen}_*_good (304 tasks): likely analogous to the Overflow cases, didn't check
  • bitvector/gcd_* (3 tasks): implicit cast signed char -> int and int -> signed char on ILP32
  • bitvector/s3_srvr_2a*.BV.c.cil (2 tasks): explicit cast int -> unsigned int and unsigned int -> int on ILP32
  • loop-invariants/even
  • array-crafted/bAnd* (5 tasks)
  • array-crafted/bor* (5 tasks)
  • array-crafted/xor* (5 tasks)
  • array-memsafety/cstrcspn-alloca-1
  • array-memsafety/cstrlen-alloca-2
  • array-memsafety/cstrspn-alloca-1
  • aws-c-common/aws_array_list_swap_harness

If the SV-COMP community decides that casts are overflows, we might want to fix these imprecisions.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions