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; diff --git a/tests/syntax/local-init-const.i b/tests/syntax/local-init-const.i new file mode 100644 index 0000000000000000000000000000000000000000..1d79724df761cbe3b412972bc0fb43c3fd156ea1 --- /dev/null +++ b/tests/syntax/local-init-const.i @@ -0,0 +1,9 @@ +/*run.config + OPT: -no-autoload-plugins -load-module eva,scope -eva -eva-verbose 0 + */ +unsigned id(unsigned x) { return x; } + +void main() { + unsigned const r = id(1 > 2 ? 1 : 2); + //@ assert written_r: r == 2; +} diff --git a/tests/syntax/oracle/local-init-const.res.oracle b/tests/syntax/oracle/local-init-const.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..98bd497cc4f331b551c25605e8c6bfd2688c1913 --- /dev/null +++ b/tests/syntax/oracle/local-init-const.res.oracle @@ -0,0 +1 @@ +[kernel] Parsing tests/syntax/local-init-const.i (no preprocessing)