Commit f0cdb661 authored by David Hauzar's avatar David Hauzar

Marking record fields that will not be shown in counterexample.

Record fields labeled with label model_trace:@hide_field will be not
shown in counterexample.
parent da802d43
......@@ -75,8 +75,11 @@ let rec add_quant kn (vl,tl,f) v =
end
| _ -> ""
) in
let label = Ident.append_to_model_element_name
~labels:v.vs_name.id_label ~to_append:(field_name) in
let label = if field_name = "@hide_field" then
Ident.remove_model_labels ~labels:v.vs_name.id_label
else
Ident.append_to_model_element_name
~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
......
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