0001553: Fails to cope with multiple non-contiguous constant array instantiations

Notes
(0005942) gergo (reporter) 2015-06-23 21:02	I stumbled across the same problem in Sodium-20150201, where it is still present. The apparent fix is trivial: --- ../frama-c-Sodium-20150201/cil/src/frontc/cabs2cil.ml 2015-03-06 16:28:27.000000000 +0100 +++ cil/src/frontc/cabs2cil.ml 2015-06-23 20:54:47.133240542 +0200 @@ -7819,7 +7819,6 @@ }; !currentFunctionFDEC.svar.vdecl <- idloc; - constrExprId := 0; (* Setup the environment. Add the formals to the locals. Maybe * they need alpha-conv ) enterScope (); ( Start the scope *) This code used to reset that counter every time a function definition was entered; removing that reset changes nothing except that it ensures that the generated __constr_expr_ variables have globally unique names (even across files). The counter is not used for anything else but for making these variable names unique. Possibly it should be reset when previously read source files are re-parsed, I don't know.

(0005990) yakobowski (manager) 2015-08-03 19:42	Your patch is correct. We arrived at the same fix a few years back, but forgot to commit it. Apologies for this... The fix will be in the next version of Frama-C. (Resetting the counter at the beginning of a file is slightly better, because the generated numbers will be more predictable.)

(0005991) yakobowski (manager) 2015-08-03 19:42	Fix committed to master branch.

Relationships