[PATCH] D12901: [Static Analyzer] Assertion "System is over constrained" after truncating 64 bits integers to 32 bits. (PR25078)

[pierre gousseau via cfe-commits]

pgousseau updated the summary for this revision.
pgousseau updated this revision to Diff 43120.
pgousseau added a comment.

Following Gabor and Anna's advice:

- Instead of modifying assumeSymNE and assumeSymEQ, this patch adds a new method 'SValBuilder::evalIntegralCast'.

The current workaround for truncations not being modelled is that the evaluation of integer to integer casts are simply bypassed and so the original symbol is used as the new casted symbol (cf SimpleSValBuilder::evalCastFromNonLoc).
This lead to the issue described above, as the RangeConstraintManager associates ranges with symbols.

The new evalIntegralCast method added by this patch wont bypass the cast if it finds the range of the symbol to be greater than the maximum value of the target type.

This patch also fixes a bug in 'RangeSet::pin' causing single value ranges to not be considered conventionally ordered.

The patch has been tested with openssl-1.0.0d-src and bullet-2.82-r2704 with no regressions observed.

Please let me know if this an acceptable change?

Regards,

Pierre Gousseau
SN Systems - Sony Computer Entertainment


http://reviews.llvm.org/D12901

Files:
  include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
  lib/StaticAnalyzer/Core/ExprEngineC.cpp
  lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  lib/StaticAnalyzer/Core/SValBuilder.cpp
  test/Analysis/range_casts.c

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D12901.43120.patch
Type: text/x-patch
Size: 9322 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20151217/67da13cd/attachment.bin>