Not appending "." to names of record fields in counterexamples.

Previously, "." was automatically appended to names stored in
model_trace label when creating variables corresponding to record
fields in eval_match and when projecting record fields in the
transformation intro_projections_counterexmp. Now, this is not done
and "." must be given in model_trace label of the projection or
record field.

The reason is that for SPARK, character different from "." (e.g., "'"
needs to be sometimes appended.

examples/tests/cvc4-models.mlw

@@ -53,13 +53,13 @@ module M
 
   (*** In all cases, records are decomposed using match eval ***)
 
-  type r = {f "model_trace:field_f" :int; g:bool}
+  type r = {f "model_trace:.field_f" :int; g:bool}
 
   (* Projection functions *)
-  function projf_r_f "model_trace:f" (x : r) : int
+  function projf_r_f "model_trace:.f" (x : r) : int
   =
   x.f
-  function projf_r_g "model_trace:g" (x : r) : bool
+  function projf_r_g "model_trace:.g" (x : r) : bool
   =
   x.g
   meta "inline : no" function projf_r_f
@@ -106,10 +106,10 @@ module M
   (*** Records and maps together ***)
   type r_map = {f_map:map bool int; g_bool:bool}
 
-  function projf_r_map_f_map "model_trace:f_map" (rec_map : r_map) : map bool int
+  function projf_r_map_f_map "model_trace:.f_map" (rec_map : r_map) : map bool int
   =
   rec_map.f_map
-  function projf_r_map_g "model_trace:g_map" (rec_map : r_map) : bool
+  function projf_r_map_g "model_trace:.g_map" (rec_map : r_map) : bool
   =
   rec_map.g_bool
   meta "inline : no" function projf_r_map_f_map
@@ -140,15 +140,15 @@ module M
   (*******************************************
    ** Definitions of projections used below **
    *******************************************)
-  function projfi "model_trace:projfi" (l : int) : int
+  function projfi "model_trace:.projfi" (l : int) : int
   = l
   meta "inline : no" function projfi
   meta "model_projection" function projfi
 
-  function projf1 "model_trace:projf1" (l : int) : bool
+  function projf1 "model_trace:.projf1" (l : int) : bool
   =
   l > 0
-  function projf2 "model_trace:projf2" (l : int) : bool
+  function projf2 "model_trace:.projf2" (l : int) : bool
   =
   l <= 0
   meta "inline : no" function projf1
@@ -180,7 +180,7 @@ module M
    *********************************)
    (* Warning: if definition of the following projections are present,
       the proof of everything below will not terminate. *)
-  function projfl "model_trace:projfl" (l : list int_type) : int
+  function projfl "model_trace:.projfl" (l : list int_type) : int
   =
   match l with
   | Nil -> 0

src/core/ident.ml

@@ -44,6 +44,12 @@ let lab_compare l1 l2 = Pervasives.compare l1.lab_tag l2.lab_tag
 
 (* functions for working with counterexample model labels *)
 
+let model_proj_label = create_label "model_projected"
+let model_label = create_label "model"
+
+let remove_model_labels ~labels =
+  Slab.filter (fun l -> (l <> model_label) && (l <> model_proj_label) ) labels
+
 let is_model_trace_label label =
   Strings.has_prefix "model_trace:" label.lab_string
 

src/core/ident.mli

@@ -29,6 +29,9 @@ val create_label : string -> label
 
 (* functions for working with counterexample model labels *)
 
+val remove_model_labels : labels : Slab.t -> Slab.t
+(** Returns a copy of labels without labels "model" and "model_projected". *)
+
 val append_to_model_trace_label : labels : Slab.t ->
   to_append : string ->
   Slab.t

src/transform/eval_match.ml

@@ -71,13 +71,12 @@ let rec add_quant kn (vl,tl,f) v =
 	      begin
 		try
 		  Ident.get_model_trace_string ~labels:pj_ls.ls_name.id_label
-		with Not_found -> pj_ls.ls_name.id_string
+		with Not_found -> "."^pj_ls.ls_name.id_string
 	      end
 	    | _ -> ""
 	  ) in
-	  let field_str = if field_name = "" then "" else "." ^ field_name in
 	  let label = Ident.append_to_model_element_name
-	    ~labels:v.vs_name.id_label ~to_append:(field_str) in
+	    ~labels:v.vs_name.id_label ~to_append:(field_name) in
 	  create_vsymbol (id_lab label v.vs_name) (ty_inst s ty) in
         let nvl = List.map2 mk_v ls.ls_args pjl in
         let t = fs_app ls (List.map t_var nvl) ty in

src/transform/intro_projections_counterexmp.ml

@@ -106,11 +106,9 @@ let intro_proj_for_ls env map_projs ls_projected =
 	   Parameter applied_proj_f is a set of projection functions already applied to the term *)
 
 	let get_record_field_suffix projection =
-	  let proj_name =
-	    try
-	      get_model_element_name ~labels:projection.ls_name.id_label
-	    with Not_found -> "" in
-	  if proj_name = "" then proj_name else "."^proj_name in
+	  try
+	    get_model_element_name ~labels:projection.ls_name.id_label
+	  with Not_found -> "" in
 
 	match (Opt.get term.t_ty).ty_node with
 	| Tyapp (ts, [t_from; t_to]) when ts.ts_name.id_string = "map" -> begin

src/whyml/mlw_wp.ml

@@ -316,15 +316,12 @@ let create_model_data ?loc ?context_labels append_to_model_trace =
     md_context_labels = context_labels;
   }
 
-let model_proj_label = Ident.create_label "model_projected"
-let model_label = Ident.create_label "model"
-
 let mk_var id ty md =
   let new_labels, loc = match md with
     | None ->
       (* If there is no model data remove model labels (prevents counter-example
 	 projections of this variable, displaying this variable in counterexample, ...) *)
-      let new_labels = Slab.filter (fun l -> (l <> model_label) && (l <> model_proj_label) ) id.id_label in
+      let new_labels = Ident.remove_model_labels ~labels:id.id_label in
       (new_labels, None)
     | Some md -> begin
       (append_to_model_trace_label ~labels:id.id_label ~to_append:("@"^md.md_append_to_model_trace), md.md_loc)