diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 89290cbc8816f5a0694977e7ba49d2ed6a279850..d2117f9eaafe055b4c7c1b5d78a9366a65e8c6e4 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -1208,6 +1208,7 @@ let get_temp_name ghost () = (* Create a new temporary variable *) let newTempVar ~ghost loc descr (descrpure:bool) typ = let t' = (!typeForInsertedVar) typ in + let t' = Cil.typeRemoveAttributes ["const"] t' in let name = get_temp_name ghost () in let vi = makeVarinfo ~ghost ~temp:true ~loc false false name t' in vi.vdescr <- Some descr;