Repository navigation
Fix incorrect results in NoOverflows-Other #27
Description
Verification tasks in SV-COMP
-
../../sv-benchmarks/c/bitvector/byte_add-2.i
Fix check for shift operation r3 << 24U, see ISO/IEC 9899:2011 6.5.7#4, in that case r3<<24U will exceed INT_MAX
-
../../sv-benchmarks/c/bitvector/byte_add_1-2.i
Not identified bug root, but we have modeling issues with shift operation
-
../../sv-benchmarks/c/bitvector/byte_add_2-1.i
Not identified bug root, but we have modeling issues with shift operation
Activity