diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.ml b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
index d337b04075cf4cf072e9d28ed1d371341bd7f76a..27a8185b7cabd368f0d4d4adea8795df51d523ae 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
@@ -67,8 +67,9 @@ let pre_funspec kf kinstr env funspec =
       funspec;
     env
   in
-  let env = convert_unsupported_clauses env in
   let loc = Kernel_function.get_location kf in
+  Cil.CurrentLoc.set loc;
+  let env = convert_unsupported_clauses env in
   let contract = Contract.create ~loc funspec in
   Env.with_rte env true
     ~f:(fun env -> Contract.translate_preconditions kf kinstr env contract)