diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog index 18e4134ca9a8c25d63757652ba3ac2c604db9395..1b49d78daec90f2f3a810c06b42327b24a4b20d2 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 78d76d732ac3f051290d4b4d20fdfa3451af158b..50ebd5558d79cf55824362d9ee840b72a5e70a40 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