From 750b20e5145902bb5c8473a95fc913cc4e0f757c Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 6 Nov 2015 18:52:07 +0100
Subject: [PATCH] fix crash occuring with a recent libc
---
src/plugins/e-acsl/doc/Changelog | 3 +++
src/plugins/e-acsl/dup_functions.ml | 3 ++-
2 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 30272295f40..5530d826bcc 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,9 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2015/11/06] Fix a crash occuring when using a recent libc
+ while GMP headers provided by E-ACSL are used.
+
########################
Plugin E-ACSL 0.5 Sodium
########################
diff --git a/src/plugins/e-acsl/dup_functions.ml b/src/plugins/e-acsl/dup_functions.ml
index 66672aa36b5..40533cbe9b3 100644
--- a/src/plugins/e-acsl/dup_functions.ml
+++ b/src/plugins/e-acsl/dup_functions.ml
@@ -341,7 +341,8 @@ if there are memory-related annotations.@]"
| Before_gmp -> before_memory_model <- Gmp
| Gmp | Memory_model -> ()
| After_gmp -> before_memory_model <- Memory_model
- | Code -> assert false);
+ | Code -> () (* still processing the GMP and memory model headers,
+ but reading some libc code *));
Cil.JustCopy
| GVarDecl(vi, _) | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
when Cil.is_builtin vi ->
--
GitLab