From b0eb180d16d1132fa2be4a7744fe389049b51af9 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon, 11 Sep 2023 15:01:20 +0200
Subject: [PATCH] Also generate assigns from prototype for definitions
---
src/kernel_internals/typing/populate_spec.ml | 5 ++---
1 file changed, 2 insertions(+), 3 deletions(-)
diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml
index 32b0492f4fe..119668f8d36 100644
--- a/src/kernel_internals/typing/populate_spec.ml
+++ b/src/kernel_internals/typing/populate_spec.ml
@@ -354,9 +354,8 @@ struct
else WritesAny
let frama_c_default kf =
- if Kernel_function.has_definition kf then
- acsl_default () (* TODO: use genassigns *)
- else Writes (Infer_annotations.assigns_from_prototype kf)
+ (* TODO: use genassigns for Definitions. *)
+ Writes (Infer_annotations.assigns_from_prototype kf)
let compare_deps d1 d2 =
match d1, d2 with
--
GitLab