Commit 4c21fd7e authored by Sylvain Dailler's avatar Sylvain Dailler

Remove unused attributes.

parent fcd1f2ae
......@@ -342,9 +342,7 @@ let sanitizer head rest n = sanitizer' head rest rest n
let proxy_attr = create_attribute "mlw:proxy_symbol"
let model_projected_attr = create_attribute "model_projected"
let model_vc_attr = create_attribute "model_vc"
let model_vc_post_attr = create_attribute "model_vc_post"
let model_vc_havoc_attr = create_attribute "model_vc_havoc"
let create_model_trace_attr s = create_attribute ("model_trace:" ^ s)
......
......@@ -170,9 +170,7 @@ val proxy_attr: attribute
(** {2 Attributes for handling counterexamples} *)
val model_projected_attr : attribute
val model_vc_attr : attribute
val model_vc_post_attr : attribute
val model_vc_havoc_attr : attribute
val has_a_model_attr : ident -> bool
(** [true] when [ident] has one of the attributes above *)
......
......@@ -408,8 +408,7 @@ let unit_module =
let itd_ref =
let tv = create_tvsymbol (id_fresh "a") in
let attrs = Sattr.singleton (create_attribute "model_trace:") in
let pj = create_pvsymbol (id_fresh ~attrs "contents") (ity_var tv) in
let pj = create_pvsymbol (id_fresh "contents") (ity_var tv) in
create_plain_record_decl ~priv:false ~mut:true (id_fresh "ref")
[tv] [true, pj] [] []
......
......@@ -152,9 +152,6 @@ let attrs_has_expl attrs =
let annot_attrs = Sattr.add stop_split (Sattr.singleton annot_attr)
(* TODO: remove this line, and use "annot_attr" instead *)
let annot_attrs = Sattr.add Ident.model_vc_attr annot_attrs
let vc_expl loc attrs expl f =
let attrs = Sattr.union annot_attrs (Sattr.union attrs f.t_attrs) in
let attrs = if attrs_has_expl attrs then attrs else Sattr.add expl attrs in
......@@ -1373,9 +1370,7 @@ let rec sp_expr kn k rdm dst = match k with
sp_and (t_and_l (cons_t_simp (t_var n) t fl)) sp in
let sp = Mpv.fold update dst t_true in
let sp = sp_exists (Mvs.keys fvs) sp in
let attrs = Ident.model_vc_havoc_attr in
let attrs = Sattr.add attrs sp.t_attrs in
let sp = t_attr_set ?loc attrs sp in
let sp = t_attr_set ?loc sp.t_attrs sp in
let add_rhs _ rhs rd = match rhs with
| Some v -> Spv.add v rd | None -> rd in
let add_rhs _ = Mpv.fold add_rhs in
......
......@@ -84,14 +84,14 @@ let check_enter_vc_term t in_goal vc_term_info =
postcondition or precondition of a function, extract the name of
the corresponding function.
*)
if in_goal && Sattr.mem Ident.model_vc_attr t.t_attrs then begin
if in_goal && Sattr.mem Ity.annot_attr t.t_attrs then begin
vc_term_info.vc_inside <- true;
vc_term_info.vc_loc <- t.t_loc
end
let check_exit_vc_term t in_goal info =
(* Check whether the term triggering VC is exited. *)
if in_goal && Sattr.mem Ident.model_vc_attr t.t_attrs then begin
if in_goal && Sattr.mem Ity.annot_attr t.t_attrs then begin
info.vc_inside <- false;
end
......
......@@ -33,7 +33,7 @@ type vc_term_info = {
}
let is_model_vc_attr l =
attr_equal l model_vc_attr || attr_equal l model_vc_post_attr
attr_equal l Ity.annot_attr || attr_equal l model_vc_post_attr
let check_enter_vc_term t info vc_loc =
(* Check whether the term that triggers VC is entered.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment