Skip to content

base invariant_fallback mishandles casts #1782

@leunam99

Description

@leunam99

When running goblint --conf conf/svcomp25.json --set ana.specification ../sv-benchmarks/c/properties/unreach-call.prp with the following file (reduced from c/weaver/popl20-prod-cons-eq.wvr-oob.c from SV-COMP), Goblint reports true because it thinks that reach_error() is dead.

extern void abort(void);
void assume_abort_if_not(int cond) {
  if(!cond) {abort();}
}

int main() {
  int n_update;

  assume_abort_if_not(n_update >= 0);
  assume_abort_if_not(n_update <= ( 4294967295UL /  sizeof (char)));

  reach_error();
}

If I remove any of the assume_aborts, replace sizeof(char) with 1UL, or change the type of n_update to unsigned long, this is no longer the case.

Metadata

Metadata

Assignees

No one assigned

    Labels

    sv-compSV-COMP (analyses, results), witnessesunsound

    Type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions