handling dereference failures

[Anthonysdu]

Hi guys, can I ask if anyone know when esbmc would fail the deference completely? There are quite a lot of warning no body for function symex::invalid_object without explicit function names in my log.

And in the deference.cpp,it says:

 else if(is_nil_expr(value))
  {
    /* Fallback if dereference failes entirely: to make this a valid formula,
     * return a failed symbol, so that this assignment gets a well typed free
     * value. */
    value = make_failed_symbol(type);
  }

[Anthonysdu]

Or:

  bool known_exhaustive = true;
  for(const expr2tc &target : points_to_set)
    known_exhaustive &= !(is_unknown2t(target) || is_invalid2t(target));

  expr2tc value;
  if(!known_exhaustive)
    value = make_failed_symbol(type);

[fbrausse]

The PR #743 did introduce the known_exhaustive check. It has some reasoning about when and why it is performed. Do you have the source code you're trying to verify?

[Anthonysdu]

The PR #743 did introduce the known_exhaustive check. It has some reasoning about when and why it is performed. Do you have the source code you're trying to verify?

thank you! I will have a look.

[Anthonysdu]

The PR #743 did introduce the known_exhaustive check. It has some reasoning about when and why it is performed. Do you have the source code you're trying to verify?

The source code is a very large project, I am wondering whether this can be a reason that esbmc is running slow.

[fbrausse]

The source code is a very large project, I am wondering whether this can be a reason that esbmc is running slow.

Without more info it's hard to say. ESBMC does print out some timing information like how long GOTO conversion/processing took, how long the slicer and encoding to the SMT solver took, etc. If you can't share the sources to be verified, you could post those numbers to at least get a feel for where bottlenecks might be.

[lucasccordeiro]

@Anthonysdu: could you please provide further information here as suggested by @fbrausse?

[Anthonysdu]

HI all, I think this is no longer the bottleneck for me, and I will update further information if it is still a problem. Thanks!

[lucasccordeiro]

@Anthonysdu: Can we close this issue?

[Anthonysdu]

Yes!