Commit 91b3eeb7 authored by Sylvain Dailler's avatar Sylvain Dailler

counterexamples: change the kind of output model_elements

Note that this should have no effect on why3
parent c7053bd6
...@@ -350,12 +350,17 @@ let create_model_element ~name ~value ~attrs ?location ?term () = ...@@ -350,12 +350,17 @@ let create_model_element ~name ~value ~attrs ?location ?term () =
let (name, type_s) = split_model_trace_name name in let (name, type_s) = split_model_trace_name name in
let me_kind = match type_s with let me_kind = match type_s with
| "result" -> Result | "result" -> Result
| "old" -> Old | _ -> Other
| _ -> Other in in
let attrs =
match term with
| None -> attrs
| Some t -> Sattr.union t.t_attrs attrs
in
let me_name = { let me_name = {
men_name = name; men_name = name;
men_kind = me_kind; men_kind = me_kind;
men_attrs = match term with | None -> attrs | Some t -> Sattr.union t.t_attrs attrs; men_attrs = attrs;
} in } in
{ {
me_name = me_name; me_name = me_name;
...@@ -368,7 +373,6 @@ let construct_name (name: string) attrs : model_element_name = ...@@ -368,7 +373,6 @@ let construct_name (name: string) attrs : model_element_name =
let (name, type_s) = split_model_trace_name name in let (name, type_s) = split_model_trace_name name in
let me_kind = match type_s with let me_kind = match type_s with
| "result" -> Result | "result" -> Result
| "old" -> Old
| _ -> Other in | _ -> Other in
{men_name = name; men_kind = me_kind; men_attrs = attrs} {men_name = name; men_kind = me_kind; men_attrs = attrs}
...@@ -654,24 +658,59 @@ let print_attrs_json (me: model_element_name) fmt = ...@@ -654,24 +658,59 @@ let print_attrs_json (me: model_element_name) fmt =
Json_base.list (fun fmt attr -> Json_base.string fmt attr.attr_string) fmt Json_base.list (fun fmt attr -> Json_base.string fmt attr.attr_string) fmt
(Sattr.elements me.men_attrs) (Sattr.elements me.men_attrs)
(* Compute the kind of a model_element using its attributes and location *)
let compute_kind (me: model_element) =
let me_kind = me.me_name.men_kind in
let location = me.me_location in
let attrs = me.me_name.men_attrs in
let me_kind =
(* We match on the attribute on the form [@at:'Old:loc:file:line]. If it
exists, depending on the location of the me, we use it or not. If it
does not we keep me_kind.
*)
match Sattr.choose (Sattr.filter (fun x -> Strings.has_prefix "at:'Old:" x.attr_string) attrs) with
| exception Not_found -> me_kind
| a ->
begin
match Strings.split ':' a.attr_string, location with
| "at" :: "'Old" :: "loc" :: file :: line_number :: [], Some location ->
let (loc_file, loc_line, _, _) =
Loc.get location
in
if loc_file = file && loc_line = int_of_string line_number then
Old
else
me_kind
| _ -> me_kind
end
in
me_kind
(* (*
** Quering the model - json ** Quering the model - json
*) *)
let print_model_element_json me_name_to_str fmt me = let print_model_element_json me_name_to_str fmt me =
let print_value fmt = let print_value fmt =
fprintf fmt "%a" print_model_value_sanit me.me_value in fprintf fmt "%a" print_model_value_sanit me.me_value
in
let print_kind fmt = let print_kind fmt =
match me.me_name.men_kind with (* We compute kinds using the attributes and locations *)
let me_kind = compute_kind me in
match me_kind with
| Result -> fprintf fmt "%a" Json_base.string "result" | Result -> fprintf fmt "%a" Json_base.string "result"
| Old -> fprintf fmt "%a" Json_base.string "old" | Old -> fprintf fmt "%a" Json_base.string "old"
| Error_message -> fprintf fmt "%a" Json_base.string "error_message" | Error_message -> fprintf fmt "%a" Json_base.string "error_message"
| Other -> fprintf fmt "%a" Json_base.string "other" in | Other -> fprintf fmt "%a" Json_base.string "other"
in
let print_name fmt = let print_name fmt =
Json_base.string fmt (me_name_to_str me) in Json_base.string fmt (me_name_to_str me)
in
let print_json_attrs fmt = let print_json_attrs fmt =
print_attrs_json me.me_name fmt in print_attrs_json me.me_name fmt
in
let print_value_or_kind_or_name fmt printer = let print_value_or_kind_or_name fmt printer =
printer fmt in printer fmt
in
Json_base.map_bindings Json_base.map_bindings
(fun s -> s) (fun s -> s)
print_value_or_kind_or_name print_value_or_kind_or_name
......
...@@ -409,7 +409,8 @@ and convert_to_model_value (t: term): Model_parser.model_value = ...@@ -409,7 +409,8 @@ and convert_to_model_value (t: term): Model_parser.model_value =
| Trees tree -> | Trees tree ->
begin match tree with begin match tree with
| [] -> raise Not_value | [] -> raise Not_value
| [field, value] -> Model_parser.Proj (field, convert_to_model_value value) | [field, value] ->
Model_parser.Proj (field, convert_to_model_value value)
| l -> | l ->
Model_parser.Record Model_parser.Record
(List.map (fun (field, value) -> (List.map (fun (field, value) ->
......
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