From c4b845a07f950a77b922549a3270ef5f636b5b85 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 26 Jun 2013 14:37:28 +0000
Subject: [PATCH] [E-ACSL] fix crash with typedef on pointer types
---
src/plugins/e-acsl/doc/Changelog | 1 +
src/plugins/e-acsl/translate.ml | 2 +-
2 files changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 18e4134ca9a..1b49d78daec 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,7 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2013/06/26] Fix crash with typedef on pointer types.
- E-ACSL [2013/06/21] Fewer unknown locations.
-* E-ACSL [2013/06/18] Fixed bug when generating RTEs on the E-ACSL
generated project.
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 78d76d732ac..50ebd5558d7 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -453,7 +453,7 @@ and mmodel_call_with_size ~loc kf name ctx env t =
None
ctx
(fun v _ ->
- let sizeof = match typ with
+ let sizeof = match Cil.unrollType typ with
| TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
| _ -> assert false
in
--
GitLab