C-Reduce doesn't not attempt to do that. Many C-Reduce transformations
can introduce UBs such as array-out-of-bound-access. As Eric says, we
use Frama-C and KCC to detect UB for C programs.
- Yang
On 7/26/13 5:49 AM, Kees Bakker wrote:
Hi,
Does anyone have suggestions how to avoid reduction that
reads/writes outside an array.
The reason I ask, after creduce is finished I get this code
uint32_t g_33[1]; // <====
uint32_t g_202[4];
int8_t
func_1 ()
{
uint32_t *l_32 = &g_33[1]; // <===
uint32_t *l_972 = &g_202[0];
++*l_32, *l_972 = g_708.f1;
return 0;
}
This fails because the program writes outside the g_33 array.
My own compiler tools have boundary checks, but this is a cross
compiler and I'm using a simulator to run the result. It's doable
but slow.
So far, with clang, gcc, valgrind I couldn't find a method to detect
array boundary violations.
(( BTW I'm not sure if this is a creduce bug. ))
