Incorrect code generation with gmp
ID0002231: This issue was created automatically from Mantis Issue 2231. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002231 | Frama-C | Plug-in > E-ACSL | public | 2016-06-14 | 2017-01-18 |
| Reporter | kvorobyov | Assigned To | signoles | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | X86-64 | OS | Linux | OS Version | - |
| Product Version | Frama-C Aluminium | Target Version | Frama-C Aluminium | Fixed in Version | Frama-C 14-Silicon |
Description :
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