Skip to content
Snippets Groups Projects
Commit 5e4de8a2 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

fix indentation

parent 374cf5ca
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/gui/property_navigator.ml
+ 104
− 104
View file @ 5e4de8a2
......@@ -34,13 +34,13 @@ let all_properties () =
match Property.get_kf ip with
| None -> globals := Property.Set.add ip !globals
| Some kf ->
if not (Ast_info.is_frama_c_builtin (Kernel_function.get_name kf))
then try
let fips = Kernel_function.Map.find kf !functions in
fips := Property.Set.add ip !fips
with Not_found ->
let ips = Property.Set.singleton ip in
functions := Kernel_function.Map.add kf (ref ips) !functions
if not (Ast_info.is_frama_c_builtin (Kernel_function.get_name kf))
then try
let fips = Kernel_function.Map.find kf !functions in
fips := Property.Set.add ip !fips
with Not_found ->
let ips = Property.Set.singleton ip in
functions := Kernel_function.Map.add kf (ref ips) !functions
);
!functions, !globals
......@@ -72,8 +72,8 @@ let make_property ip =
in
let function_name, module_name = match Property.get_kf ip with
| None -> "", Datatype.Filepath.dummy (* TODO: it would be great to find the location
of global invariants or lemmas, but there isn't
enough information in the ast *)
of global invariants or lemmas, but there isn't
enough information in the ast *)
| Some kf -> kf_name_and_module kf
in
let kind =
......@@ -409,31 +409,31 @@ let aux_rte kf acc (name, _, rte_status_get: Db.RteGen.status_accessor) =
match st, rteGenerated.get (), rteNotGenerated.get () with
| true, true, _
| false, _, true ->
(* Considered that leaf functions are not verified internally *)
let status_name, status =
if st then
if Kernel_function.is_definition kf
then "Generated", Feedback.Valid
else "Considered generated", Feedback.Considered_valid
else "Not generated", Feedback.Invalid
in
let function_name, module_name = kf_name_and_module kf in
let status_icon = Gtk_helper.Icon.Feedback status in
let ip =
Property.ip_other name
(Property.OLGlob (Kernel_function.get_location kf))
in
{
module_name = module_name;
function_name = function_name;
visible = true;
ip=ip;
kind=Format.asprintf "@[<hov>%a@]" Property.pretty ip;
status_name = "" ;
consolidated_status = None ;
consolidated_status_name = status_name ;
status_icon = status_icon ;
} :: acc
(* Considered that leaf functions are not verified internally *)
let status_name, status =
if st then
if Kernel_function.is_definition kf
then "Generated", Feedback.Valid
else "Considered generated", Feedback.Considered_valid
else "Not generated", Feedback.Invalid
in
let function_name, module_name = kf_name_and_module kf in
let status_icon = Gtk_helper.Icon.Feedback status in
let ip =
Property.ip_other name
(Property.OLGlob (Kernel_function.get_location kf))
in
{
module_name = module_name;
function_name = function_name;
visible = true;
ip=ip;
kind=Format.asprintf "@[<hov>%a@]" Property.pretty ip;
status_name = "" ;
consolidated_status = None ;
consolidated_status_name = status_name ;
status_icon = status_icon ;
} :: acc
| true, false, _
| false, _, false -> acc
......@@ -533,7 +533,7 @@ let make_panel (main_ui:main_window_extension_points) =
match !properties_tab_label with
| None -> ()
| Some label ->
GtkMisc.Label.set_text label "Properties"
GtkMisc.Label.set_text label "Properties"
);
let sc =
GBin.scrolled_window
......@@ -552,10 +552,10 @@ let make_panel (main_ui:main_window_extension_points) =
~callback:(fun path _col ->
match model#custom_get_iter path with
| Some { MODEL.finfo = { ip = ip } } ->
let format_graph ppf =
Consolidation_graph.dump (Consolidation_graph.get ip) ppf in
Dgraph_helper.graph_window_through_dot
main_ui#main_window "Dependencies" format_graph
let format_graph ppf =
Consolidation_graph.dump (Consolidation_graph.get ip) ppf in
Dgraph_helper.graph_window_through_dot
main_ui#main_window "Dependencies" format_graph
| None -> ()));
view#selection#set_select_function
(fun path currently_selected ->
......@@ -598,7 +598,7 @@ let make_panel (main_ui:main_window_extension_points) =
(* Status colored column viewer *)
make_view_column (GTree.cell_renderer_pixbuf [top])
(function {status_icon=status_icon} ->
[`PIXBUF (Gtk_helper.Icon.get status_icon)])
[`PIXBUF (Gtk_helper.Icon.get status_icon)])
~title:"Status";
(* Consolidated status name column viewer *)
......@@ -620,14 +620,14 @@ let make_panel (main_ui:main_window_extension_points) =
| IPBehavior {ib_kinstr=Kglobal} -> behaviors.get ()
| IPBehavior {ib_kinstr=Kstmt _} -> behaviors.get () && stmtSpec.get ()
| IPPredicate {ip_kind=PKRequires _;ip_kinstr=Kglobal} ->
preconditions.get ()
preconditions.get ()
| IPPredicate {ip_kind=PKRequires _;ip_kinstr=Kstmt _} ->
preconditions.get () && stmtSpec.get ()
preconditions.get () && stmtSpec.get ()
| IPPredicate {ip_kind = PKAssumes _} -> false
| IPPredicate {ip_kind=PKEnsures _;ip_kinstr=Kglobal} -> ensures.get ()
| IPExtended _ -> extended.get ()
| IPPredicate {ip_kind=PKEnsures _;ip_kinstr=Kstmt _} ->
ensures.get() && stmtSpec.get()
ensures.get() && stmtSpec.get()
| IPPredicate {ip_kind = PKTerminates} -> terminates.get ()
| IPAxiom _ -> false
| IPTypeInvariant _ -> typeInvariants.get()
......@@ -646,20 +646,20 @@ let make_panel (main_ui:main_window_extension_points) =
| Check -> user_checks.get ()
end
| IPCodeAnnot {ica_ca={annot_content = AInvariant _}} ->
invariant.get ()
invariant.get ()
| IPCodeAnnot {ica_ca={annot_content = APragma p}} ->
Logic_utils.is_property_pragma p (* currently always false. *)
Logic_utils.is_property_pragma p (* currently always false. *)
| IPCodeAnnot _ -> false (* status of inner nodes *)
| IPAllocation {ial_kinstr=Kglobal} -> allocations.get ()
| IPAllocation {ial_kinstr=Kstmt _;ial_bhv=Id_loop _} ->
allocations.get ()
allocations.get ()
| IPAllocation {ial_kinstr=Kstmt _;ial_bhv=Id_contract _} ->
allocations.get() && stmtSpec.get()
allocations.get() && stmtSpec.get()
| IPAssigns {ias_kinstr=Kglobal} -> assigns.get ()
| IPAssigns {ias_kinstr=Kstmt _;ias_bhv=Id_loop _} ->
assigns.get ()
assigns.get ()
| IPAssigns {ias_kinstr=Kstmt _;ias_bhv=Id_contract _} ->
assigns.get() && stmtSpec.get()
assigns.get() && stmtSpec.get()
| IPFrom _ -> from.get ()
| IPDecrease _ -> variant.get ()
| IPPropertyInstance _ -> instances.get ()
......@@ -696,7 +696,7 @@ let make_panel (main_ui:main_window_extension_points) =
List.exists
(function
| GFun ({svar = fvi},_) | GFunDecl (_, fvi, _) ->
Cil_datatype.Varinfo.equal fvi kfvi
Cil_datatype.Varinfo.equal fvi kfvi
| _ -> false
) main_ui#file_tree#selected_globals)
in
......@@ -736,8 +736,8 @@ let make_panel (main_ui:main_window_extension_points) =
match !properties_tab_label with
| None -> ()
| Some label ->
let text = Format.sprintf "Properties (%d)" (model#custom_iter_n_children None) in
GtkMisc.Label.set_text label text
let text = Format.sprintf "Properties (%d)" (model#custom_iter_n_children None) in
GtkMisc.Label.set_text label text
in
ignore
(let callback _ =
......@@ -764,62 +764,62 @@ let make_panel (main_ui:main_window_extension_points) =
let highlighter (buffer:reactive_buffer) localizable ~start ~stop =
match localizable with
| Pretty_source.PIP ppt ->
if Property.has_status ppt then
Design.Feedback.mark
buffer#buffer ~offset:start (Property_status.Feedback.get ppt)
if Property.has_status ppt then
Design.Feedback.mark
buffer#buffer ~offset:start (Property_status.Feedback.get ppt)
| Pretty_source.PStmt(_,({ skind=Instr(Call _| Local_init (_, ConsInit _, _)) } as stmt)) ->
let kfs = Statuses_by_call.all_functions_with_preconditions stmt in
(* We separate the consolidated statuses of the preconditions inside
guarded behaviors from those outside. For guarded behaviors, since we
do not keep track of the status of 'assumes' clauses, we cannot know
if they are active. Hence, we must weaken any 'Invalid' status into
'Unknown'. *)
let filter (ip_src, _ip_copy) =
match ip_src with
let kfs = Statuses_by_call.all_functions_with_preconditions stmt in
(* We separate the consolidated statuses of the preconditions inside
guarded behaviors from those outside. For guarded behaviors, since we
do not keep track of the status of 'assumes' clauses, we cannot know
if they are active. Hence, we must weaken any 'Invalid' status into
'Unknown'. *)
let filter (ip_src, _ip_copy) =
match ip_src with
| Property.IPPredicate {Property.ip_kind=Property.PKRequires bhv} ->
bhv.b_assumes = []
| _ -> false
bhv.b_assumes = []
| _ -> false
in
let ips_sure, ips_unsure = Kernel_function.Hptset.fold
(fun kf (ips_sure, ips_unsure) ->
Statuses_by_call.setup_all_preconditions_proxies kf;
let ips_kf =
Statuses_by_call.all_call_preconditions_at ~warn_missing:false kf stmt
in
let ips_kf_sure, ips_kf_unsure = List.partition filter ips_kf in
(List.map snd ips_kf_sure @ ips_sure),
(List.map snd ips_kf_unsure @ ips_unsure))
kfs ([], [])
in
let ips = ips_sure @ ips_unsure in
if ips <> [] then
let validity = Property_status.Feedback.get_conjunction ips in
let validity =
match validity with
| Feedback.Invalid_under_hyp ->
(* Weaken if the invalidity comes from [ips_unsure]. We do nothing
for statuses [Invalid] (a path should exist, hence the behavior
must be active), or [Invalid_but_dead] (equivalent to [True]) *)
let invalid ip = Feedback.get ip = Feedback.Invalid_under_hyp in
if List.exists invalid ips_unsure &&
not (List.exists invalid ips_sure)
then Feedback.Unknown
else validity
| _ -> validity
in
let ips_sure, ips_unsure = Kernel_function.Hptset.fold
(fun kf (ips_sure, ips_unsure) ->
Statuses_by_call.setup_all_preconditions_proxies kf;
let ips_kf =
Statuses_by_call.all_call_preconditions_at ~warn_missing:false kf stmt
in
let ips_kf_sure, ips_kf_unsure = List.partition filter ips_kf in
(List.map snd ips_kf_sure @ ips_sure),
(List.map snd ips_kf_unsure @ ips_unsure))
kfs ([], [])
(* Positioning the bullet is tricky. We cannot use [start] as offset,
because the bullet ends up at the beginning of the spec (assertions,
contracts, etc) instead of in front of the function name. We use
the beginning of the C part of the statement (which has been computed
when the source was rendered). *)
let offset =
try Pretty_source.stmt_start buffer#locs stmt
with Not_found ->
Gui_parameters.error
"Invalid internal state for statement %d" stmt.sid;
stop (* fallback *)
in
let ips = ips_sure @ ips_unsure in
if ips <> [] then
let validity = Property_status.Feedback.get_conjunction ips in
let validity =
match validity with
| Feedback.Invalid_under_hyp ->
(* Weaken if the invalidity comes from [ips_unsure]. We do nothing
for statuses [Invalid] (a path should exist, hence the behavior
must be active), or [Invalid_but_dead] (equivalent to [True]) *)
let invalid ip = Feedback.get ip = Feedback.Invalid_under_hyp in
if List.exists invalid ips_unsure &&
not (List.exists invalid ips_sure)
then Feedback.Unknown
else validity
| _ -> validity
in
(* Positioning the bullet is tricky. We cannot use [start] as offset,
because the bullet ends up at the beginning of the spec (assertions,
contracts, etc) instead of in front of the function name. We use
the beginning of the C part of the statement (which has been computed
when the source was rendered). *)
let offset =
try Pretty_source.stmt_start buffer#locs stmt
with Not_found ->
Gui_parameters.error
"Invalid internal state for statement %d" stmt.sid;
stop (* fallback *)
in
Design.Feedback.mark buffer#buffer ~call_site:stmt ~offset validity
Design.Feedback.mark buffer#buffer ~call_site:stmt ~offset validity
| Pretty_source.PStmt _ | Pretty_source.PStmtStart _
| Pretty_source.PGlobal _| Pretty_source.PVDecl _
......
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