diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml index 960e1d79cb5658576b7c7477da82e33c4a3457e7..49f1da4d1c25f2bacb000c77510c3eaef337784e 100644 --- a/src/plugins/e-acsl/src/code_generator/injector.ml +++ b/src/plugins/e-acsl/src/code_generator/injector.ml @@ -465,7 +465,6 @@ and inject_in_stmt env kf stmt = (* translate the precondition of the function *) let env = if translate_pre_funspec then begin - Populate_spec.(populate_funspec kf [`Assigns]); let funspec = Annotations.funspec kf in Translate_annots.pre_funspec kf env funspec end