diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 8481d90b3a09bc2957a0ecd56b8f2a4de304763d..3b5d8650f347264b008925e1ed2201afce0a935f 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -1175,10 +1175,11 @@ let get_temp_name ?(ghost=false) () = name (* Create a new temporary variable *) -let newTempVar ~ghost descr (descrpure:bool) typ = +let newTempVar ~ghost loc descr (descrpure:bool) typ = let t' = (!typeForInsertedVar) typ in let name = get_temp_name ~ghost () in let vi = makeVarinfo ~ghost ~temp:true false false name t' in + vi.vdecl <- loc; vi.vdescr <- Some descr; vi.vdescrpure <- descrpure; alphaConvertVarAndAddToEnv false vi @@ -1566,7 +1567,8 @@ struct match Cil_datatype.Varinfo.Hashtbl.find_opt replacements vi with | None -> let vi' = - newTempVar (vi.vname ^ " initialization") ~ghost true vi.vtype + newTempVar + ~ghost vi.vdecl (vi.vname ^ " initialization") true vi.vtype in Cil_datatype.Varinfo.Hashtbl.add replacements vi vi'; vars := vi' :: !vars; @@ -6176,7 +6178,7 @@ and doExp local_env Format.asprintf "%a%s" Cil_descriptive_printer.pp_exp e' (if uop = A.POSINCR then "++" else "--") in - let tmp = newTempVar ~ghost descr true t in + let tmp = newTempVar ~ghost loc descr true t in ([var tmp], local_var_chunk se' tmp +++ (mkStmtOneInstr ~ghost:local_env.is_ghost ~valid_sid @@ -6258,7 +6260,7 @@ and doExp local_env let descr = Format.asprintf "%a" Cil_descriptive_printer.pp_lval lv in - let tmp = newTempVar ~ghost descr true lvt in + let tmp = newTempVar ~ghost loc descr true lvt in let chunk = i2c (mkStmtOneInstr ~ghost:local_env.is_ghost ~valid_sid @@ -6380,7 +6382,7 @@ and doExp local_env finishExp [] se e' intType | _ -> let tmp = - newTempVar ~ghost "<boolean expression>" true intType + newTempVar ~ghost loc "<boolean expression>" true intType in let condChunk = compileCondExp ~ghost ce @@ -6738,7 +6740,7 @@ and doExp local_env match !pwhat with | ASet (is_real,lv, r, lvt) -> is_real, lv, r, lvt | _ -> - let v = newTempVar ~ghost "vararg" true resTyp in + let v = newTempVar ~ghost loc "vararg" true resTyp in locals := v::!locals; false, var v, [], resTyp in @@ -7054,8 +7056,7 @@ and doExp local_env Cil_descriptive_printer.pp_exp) !pargs in - let tmp = newTempVar ~ghost descr false restype'' in - tmp.vdecl <- loc; + let tmp = newTempVar ~ghost loc descr false restype'' in locals:=tmp::!locals; (* Remember that this variable has been created for this * specific call. We will use this in collapseCallCast. *) @@ -7194,7 +7195,7 @@ and doExp local_env let descr = Format.asprintf "%a" Cprint.print_expression e1 in - let tmp = newTempVar ~ghost descr true tresult in + let tmp = newTempVar ~ghost loc descr true tresult in let tmp_var = var tmp in let tmp_lval = new_exp ~loc:e.expr_loc (Lval (tmp_var)) in let (r1, se1, _, _) = @@ -7263,7 +7264,7 @@ and doExp local_env let descr = Format.asprintf "%a" Cprint.print_expression e1 in - let tmp = newTempVar ~ghost descr true tresult in + let tmp = newTempVar ~ghost loc descr true tresult in let tmp_var = var tmp in let tmp_lval = new_exp ~loc:e.expr_loc (Lval (tmp_var)) in let (r1,se1, _, _) = @@ -7292,7 +7293,7 @@ and doExp local_env Cil_descriptive_printer.pp_exp e2' Cil_descriptive_printer.pp_exp e3' in - let tmp = newTempVar ~ghost descr true tresult in + let tmp = newTempVar ~ghost loc descr true tresult in false, var tmp, [], tresult, local_var_chunk empty tmp in @@ -7365,7 +7366,7 @@ and doExp local_env let se, e = match se.stmts with | [ { skind = Block b},_, _, _, _ ] -> - let vi = newTempVar ~ghost "GNU.body" true t in + let vi = newTempVar ~ghost loc "GNU.body" true t in b.bstmts <- b.bstmts @ [Cil.mkStmtOneInstr ~ghost:local_env.is_ghost ~valid_sid @@ -8565,7 +8566,10 @@ and cleanup_autoreference vi chunk = | Some v' -> ChangeTo v' | None -> let ghost = v.vghost in - let v' = newTempVar ~ghost (vi.vname ^ " initialization") true vi.vtype in + let loc = v.vdecl in + let v' = + newTempVar ~ghost loc (vi.vname ^ " initialization") true vi.vtype + in temp := Some v'; ChangeTo v' end else SkipChildren @@ -8765,7 +8769,7 @@ and createLocal ghost ((_, sto, _, _) as specs) (* do it in two *) let rt, _, _, _ = splitFunctionType alloca.vtype in let tmp = - newTempVar ~ghost + newTempVar ~ghost loc (Format.asprintf "alloca(%a)" Cil_printer.pp_exp alloca_size) false rt in