Merge branch 'fix/kernel/const-temporary-variable' into 'master'

[kernel] Cabs2cil: do not create const temporary variables.

Closes #966

See merge request frama-c/frama-c!2885

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;

tests/syntax/local-init-const.i

+/*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;
+}

tests/syntax/oracle/local-init-const.res.oracle

+[kernel] Parsing tests/syntax/local-init-const.i (no preprocessing)