From 52fb85f36c49597a769e336d6ef87c9e83599752 Mon Sep 17 00:00:00 2001
From: Michele Alberti <mic.alberti@gmail.com>
Date: Tue, 18 Jul 2017 18:09:43 +0200
Subject: [PATCH] Update due to logic label typing.
---
src/plugins/e-acsl/label.ml | 8 ++++----
src/plugins/e-acsl/translate.ml | 24 +++++++++++++-----------
2 files changed, 17 insertions(+), 15 deletions(-)
diff --git a/src/plugins/e-acsl/label.ml b/src/plugins/e-acsl/label.ml
index b4910eab15b..df993004097 100644
--- a/src/plugins/e-acsl/label.ml
+++ b/src/plugins/e-acsl/label.ml
@@ -81,17 +81,17 @@ let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
let get_stmt vis = function
| StmtLabel { contents = stmt } -> stmt
- | LogicLabel(_, label) when label = "Here" ->
+ | LogicLabel(_, Here) ->
(match vis#current_stmt with
| None -> Error.not_yet "label \"Here\" in function contract"
| Some s -> s)
- | LogicLabel(_, label) when label = "Old" || label = "Pre" ->
+ | LogicLabel(_, (Old | Pre)) ->
(try Kernel_function.find_first_stmt (Extlib.the vis#current_kf)
with Kernel_function.No_Statement -> assert false)
- | LogicLabel(_, label) when label = "Post" ->
+ | LogicLabel(_, Post) ->
(try Kernel_function.find_return (Extlib.the vis#current_kf)
with Kernel_function.No_Statement -> assert false)
- | LogicLabel(_, _label) -> assert false
+ | LogicLabel(_, (LoopEntry | LoopCurrent | Init | AbsLabel _)) -> assert false
(*
Local Variables:
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index f3a85b99837..5433d573730 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -468,7 +468,7 @@ and context_insensitive_term_to_exp kf env t =
let res3 = term_to_exp kf (Env.push env2) t3 in
let e, env = conditional_to_exp loc (Some t) e1 res2 res3 in
e, env, false, ""
- | Tat(t, LogicLabel(_, label)) when label = "Here" ->
+ | Tat(t, LogicLabel(_, Here)) ->
let e, env = term_to_exp kf env t in
e, env, false, ""
| Tat(t', label) ->
@@ -476,13 +476,13 @@ and context_insensitive_term_to_exp kf env t =
let e, env = term_to_exp kf (Env.push env) t' in
let e, env, is_mpz_string = at_to_exp env (Some t) label e in
e, env, is_mpz_string, ""
- | Tbase_addr(LogicLabel(_, label), t) when label = "Here" ->
+ | Tbase_addr(LogicLabel(_, Here), t) ->
mmodel_call ~loc kf "base_addr" Cil.voidPtrType env t
| Tbase_addr _ -> not_yet env "labeled \\base_addr"
- | Toffset(LogicLabel(_, label), t) when label = "Here" ->
+ | Toffset(LogicLabel(_, Here), t) ->
mmodel_call ~loc kf "offset" Cil.intType env t
| Toffset _ -> not_yet env "labeled \\offset"
- | Tblock_length(LogicLabel(_, label), t) when label = "Here" ->
+ | Tblock_length(LogicLabel(_, Here), t) ->
mmodel_call ~loc kf "block_length" Cil.ulongType env t
| Tblock_length _ -> not_yet env "labeled \\block_length"
| Tnull -> Cil.mkCast (Cil.zero ~loc) (TPtr(TVoid [], [])), env, false, "null"
@@ -647,8 +647,10 @@ and at_to_exp env t_opt label e =
Env.pop_and_get new_env new_stmt ~global_clear:false Env.Middle
in
let pre = match label with
- | LogicLabel(_, s) when s = "Here" || s = "Post" -> true
- | StmtLabel _ | LogicLabel _ -> false
+ | LogicLabel(_, (Here | Post)) -> true
+ | LogicLabel (_, (Old | Pre | LoopEntry | LoopCurrent | Init))
+ | LogicLabel (_, AbsLabel _) -> false
+ | StmtLabel _ -> false
in
env_ref := Env.extend_stmt_in_place new_env stmt ~pre block;
Cil.ChangeTo stmt
@@ -715,7 +717,7 @@ and named_predicate_content_to_exp ?name kf env p =
conditional_to_exp loc None e1 res2 res3
| Plet _ -> not_yet env "let _ = _ in _"
| Pforall _ | Pexists _ -> Quantif.quantif_to_exp kf env p
- | Pat(p, LogicLabel(_, label)) when label = "Here" ->
+ | Pat(p, LogicLabel(_, Here)) ->
named_predicate_to_exp kf env p
| Pat(p', label) ->
(* convert [t'] to [e] in a separated local env *)
@@ -723,8 +725,8 @@ and named_predicate_content_to_exp ?name kf env p =
let e, env, is_string = at_to_exp env None label e in
assert (not is_string);
e, env
- | Pvalid_read(LogicLabel(_, label) as llabel, t) as pc
- | (Pvalid(LogicLabel(_, label) as llabel, t) as pc) when label = "Here" ->
+ | Pvalid_read(LogicLabel(_, Here) as llabel, t) as pc
+ | (Pvalid(LogicLabel(_, Here) as llabel, t) as pc) ->
let call_valid t =
let name = match pc with
| Pvalid _ -> "valid"
@@ -752,7 +754,7 @@ and named_predicate_content_to_exp ?name kf env p =
end
| Pvalid _ -> not_yet env "labeled \\valid"
| Pvalid_read _ -> not_yet env "labeled \\valid_read"
- | Pinitialized(LogicLabel(_, label), t) when label = "Here" ->
+ | Pinitialized(LogicLabel(_, Here), t) ->
(match t.term_node with
(* optimisation when we know that the initialisation is ok *)
| TAddrOf (TResult _, TNoOffset) -> Cil.one ~loc, env
@@ -762,7 +764,7 @@ and named_predicate_content_to_exp ?name kf env p =
| _ -> mmodel_call_with_size ~loc kf "initialized" Cil.intType env t)
| Pinitialized _ -> not_yet env "labeled \\initialized"
| Pallocable _ -> not_yet env "\\allocate"
- | Pfreeable(LogicLabel(_, label), t) when label = "Here" ->
+ | Pfreeable(LogicLabel(_, Here), t) ->
let res, env, _, _ = mmodel_call ~loc kf "freeable" Cil.intType env t in
res, env
| Pfreeable _ -> not_yet env "labeled \\freeable"
--
GitLab