From d3026797bc0332a8fe352b458d7d820384796081 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 20 Oct 2020 15:37:18 +0200
Subject: [PATCH] [From] Fixes a crash when the main function has no body.
---
src/plugins/from/callwise.ml | 15 +++++++--------
1 file changed, 7 insertions(+), 8 deletions(-)
diff --git a/src/plugins/from/callwise.ml b/src/plugins/from/callwise.ml
index 38efe4f744c..71038fdbbc6 100644
--- a/src/plugins/from/callwise.ml
+++ b/src/plugins/from/callwise.ml
@@ -68,14 +68,13 @@ let call_for_individual_froms (call_type, value_initial_state, call_stack) =
if From_parameters.ForceCallDeps.get () then begin
let current_function, call_site = List.hd call_stack in
let register_from froms =
- try
- let { table_for_calls = table } = List.hd !call_froms_stack in
- merge_call_froms table call_site froms;
- record_callwise_dependencies_in_db call_site froms;
- with Failure _ ->
- From_parameters.fatal
- "calldeps internal error 23 empty callfromsstack %a"
- Kernel_function.pretty current_function
+ record_callwise_dependencies_in_db call_site froms;
+ match !call_froms_stack with
+ | { table_for_calls } :: _ ->
+ merge_call_froms table_for_calls call_site froms;
+ | [] ->
+ (* Empty call stack: this is the main entry point with no call site. *)
+ assert (call_site = Cil_types.Kglobal);
in
let compute_from_behaviors bhv =
let assigns = Ast_info.merge_assigns bhv in
--
GitLab