From 93493dc2715ef257700d6844a42f4d7688cd4f79 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 1 Sep 2022 09:28:57 +0200
Subject: [PATCH] [Eva] Fixes a crash on recursive functions with a
specification but no assigns.
---
src/plugins/eva/engine/recursion.ml | 14 ++++++++++++++
1 file changed, 14 insertions(+)
diff --git a/src/plugins/eva/engine/recursion.ml b/src/plugins/eva/engine/recursion.ml
index 4668713a370..88365a5169f 100644
--- a/src/plugins/eva/engine/recursion.ml
+++ b/src/plugins/eva/engine/recursion.ml
@@ -44,6 +44,11 @@ let mark_unknown_requires kinstr kf funspec =
in
List.iter emit_behavior funspec.spec_behavior
+let need_assigns funspec =
+ match Cil.find_default_behavior funspec with
+ | None -> true
+ | Some bhv -> bhv.b_assigns = WritesAny
+
let get_spec kinstr kf =
let funspec = Annotations.funspec ~populate:false kf in
if List.for_all (fun b -> b.b_assigns = WritesAny) funspec.spec_behavior
@@ -75,6 +80,15 @@ let get_spec kinstr kf =
(if depth > 0 then Format.asprintf " of depth %i" depth else "")
Kernel_function.pretty kf
in
+ let funspec =
+ if need_assigns funspec
+ then
+ begin
+ ignore (!Annotations.populate_spec_ref kf funspec);
+ Annotations.funspec ~populate:false kf
+ end
+ else funspec
+ in
mark_unknown_requires kinstr kf funspec;
funspec
--
GitLab