diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml index 2f191f1a35c64504ade1430e2855676f0f189a44..f6f97ee07f9b8390f519e0bee8d81b7da3c21483 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