-
Notifications
You must be signed in to change notification settings - Fork 277
Closed
Labels
Description
Support for SIMD arithmetic operators (e.g., addition or logical operators) exists in CBMC but this is not the case for comparison operators ==
, !=
, <
, >
, <=
and >=
. According to GCC online docs vectors are compared element by element producing a 0 when the comparison is false and -1 otherwise.
I am not able to provide an example since #5903 does not allow to compile, but this is the warning I am getting from CBMC when I run it on code that we generate:
warning: ignoring =
* type: array
* #source_location: nil
* size: constant
* type: signedbv
* width: 64
* #c_type: signed_long_int
* value: 2
0: signedbv
* width: 64
* #c_type: signed_long_int
0: array
* type: array
* #source_location: nil
* size: constant
* type: signedbv
* width: 64
* #c_type: signed_long_int
* value: 2
0: signedbv
* width: 64
* #c_type: signed_long_int
0: constant
* type: signedbv
* width: 64
* #c_type: signed_long_int
* value: 0
1: constant
* type: signedbv
* width: 64
* #c_type: signed_long_int
* value: 0
1: array
* type: array
* #source_location: nil
* size: constant
* type: signedbv
* width: 64
* #c_type: signed_long_int
* value: 2
0: signedbv
* width: 64
* #c_type: signed_long_int
0: constant
* type: signedbv
* width: 64
* #c_type: signed_long_int
* value: 0
1: constant
* type: signedbv
* width: 64
* #c_type: signed_long_int
* value: 0