Incorrect code generation with gmp
ID0002231: This issue was created automatically from Mantis Issue 2231. Further discussion may take place here.
|Plug-in > E-ACSL
|Fixed in Version
In some tricky cases involving multiple casts gmp-generated code is incorrect which leads to segmentation faults due to improper use of gmp library.
For instance, in the example (see attached file) the following code is generated:
unsigned long __gen_e_acsl_cast; mpz_t __gen_e_acsl__2; ... __gmpz_sub(__gen_e_acsl_sub,(__mpz_struct const *)__gen_e_acsl_cast, (__mpz_struct const *)(__gen_e_acsl__2));
This results in a segmentation fault because __gmpz_sub expects a mpz_t, not an integer.
Steps To Reproduce :
The attached file is instrumented with E-ACSL, compiled and executed