Update due to logic label typing.

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:

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"