From 85b26def40ce02dffb9677f26026bcd8f1d41365 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Wed, 22 Mar 2017 15:47:50 +0100
Subject: [PATCH] Update translate.ml to handle constants in expressions when
generating addresses
---
src/plugins/e-acsl/translate.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 2f191f1a35c..f6f97ee07f9 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -593,7 +593,7 @@ and mmodel_call_valid ~loc kf name ctx env t =
let e, env = term_to_exp kf (Env.rte env true) t in
let base, _ = Misc.ptr_index ~loc e in
let base_addr = match base.enode with
- | AddrOf _ -> e
+ | AddrOf _ | Const _ -> base
| Lval(lv) | StartOf(lv) -> Cil.mkAddrOf ~loc lv
| _ -> assert false
in
--
GitLab