From d130f45314c2de631b38dc31999976d9d684bf82 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 16 Nov 2012 17:53:11 +0000
Subject: [PATCH] [E-ACSL] do not crash anymore when there is no main entry
point
---
src/plugins/e-acsl/visit.ml | 10 ++++++++--
1 file changed, 8 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index efbf04fa106..3d3ec83a7a9 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -313,8 +313,14 @@ class e_acsl_visitor prj generate = object (self)
assert false
method private is_main old_kf =
- let main, _ = Globals.entry_point () in
- Kernel_function.equal old_kf main
+ try
+ let main, _ = Globals.entry_point () in
+ Kernel_function.equal old_kf main
+ with Globals.No_such_entry_point s ->
+ Options.warning ~once:true "%s@ \
+@[The generated program may be incomplete.@]"
+ s;
+ false
method vstmt_aux stmt =
Options.debug ~level:2 "proceeding stmt (sid %d) %a@."
--
GitLab