From 60a79b6e434568c55b24d96031c09db41f2e3090 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue, 12 Sep 2023 14:42:28 +0200
Subject: [PATCH] Remove spec generation, not needed here
---
src/plugins/e-acsl/src/code_generator/injector.ml | 1 -
1 file changed, 1 deletion(-)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 960e1d79cb5..49f1da4d1c2 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
--
GitLab