sig
  val is_writing_memory : Cil_types.varinfo -> bool
  val update_memory_model :
    loc:Cil_types.location ->
    ?result:Cil_types.lval ->
    Env.t ->
    Cil_types.kernel_function ->
    Cil_types.varinfo -> Cil_types.exp list -> Cil_types.lval option * Env.t
end