diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml index 37ab6859940cdf1b5060f3098ceaa34f406c7f4e..213095c8c136ebb9bf6f82b677df61ca50d344bb 100644 --- a/src/plugins/eva/engine/compute_functions.ml +++ b/src/plugins/eva/engine/compute_functions.ml @@ -82,8 +82,6 @@ let generate_specs () = Self.warning "Generating potentially incorrect assigns \ for function '%a' for which option %s is set" Kernel_function.pretty kf Parameters.UsePrototype.option_name; - (* The function populate_funspec may emit a warning. Position a loc. *) - Cil.CurrentLoc.set (Kernel_function.get_location kf); Populate_spec.populate_funspec ~do_body:true kf [`Assigns]; end in