Skip to content
Snippets Groups Projects
Commit 6ead6d86 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

lint some files

parent d295142b
No related branches found
No related tags found
No related merge requests found
......@@ -18,4 +18,4 @@
/tests/*/result
/tests/test_config_prove
/tests/*/result_prove
/top
\ No newline at end of file
/top
......@@ -39,14 +39,14 @@ let generate_spec needed _ _ _ =
Cil_types.Writes [ Logic_const.new_identified_term t, From [] ]
in {
spec_behavior = [ {
b_name = Cil.default_behavior_name ;
b_requires = [] ;
b_assumes = [] ;
b_post_cond = [] ;
b_assigns = assigns ;
b_allocation = FreeAllocAny ;
b_extended = []
} ] ;
b_name = Cil.default_behavior_name ;
b_requires = [] ;
b_assumes = [] ;
b_post_cond = [] ;
b_assigns = assigns ;
b_allocation = FreeAllocAny ;
b_extended = []
} ] ;
spec_variant = None ;
spec_terminates = None ;
spec_complete_behaviors = [] ;
......
......@@ -6,15 +6,15 @@ class print =
method! vglob_aux g =
begin match g with
| GFun(fd, _) ->
Kernel.feedback "%a is%s ghost"
Cil_datatype.Varinfo.pretty fd.svar
(if fd.svar.vghost then "" else " not")
| GFunDecl(_, vi, _) ->
Kernel.feedback "%a is%s ghost"
Cil_datatype.Varinfo.pretty vi
(if vi.vghost then "" else " not")
| _ -> ()
| GFun(fd, _) ->
Kernel.feedback "%a is%s ghost"
Cil_datatype.Varinfo.pretty fd.svar
(if fd.svar.vghost then "" else " not")
| GFunDecl(_, vi, _) ->
Kernel.feedback "%a is%s ghost"
Cil_datatype.Varinfo.pretty vi
(if vi.vghost then "" else " not")
| _ -> ()
end ;
Cil.DoChildren
......
......@@ -70,15 +70,15 @@ let run () =
Property_status.iter (fun x ->
match Wpo.goals_of_property x with
| h :: _ ->
inter_po := Wpo.{
po_gid = "";
po_sid = "";
po_name = "";
po_idx = Function(kf, None);
po_model = model;
po_pid = h.po_pid;
po_formula = Wpo.GoalAnnot vc_annot;
}
inter_po := Wpo.{
po_gid = "";
po_sid = "";
po_name = "";
po_idx = Function(kf, None);
po_model = model;
po_pid = h.po_pid;
po_formula = Wpo.GoalAnnot vc_annot;
}
| _ -> ()
);
spawn !inter_po;
......
......@@ -19,9 +19,9 @@ class nop =
| Multi _
| Inside _
| Clause _ ->
feedback#set_title "NOP" ;
feedback#set_descr "Does nothing; just for testing." ;
Applicable (fun s -> ["Nop", s])
feedback#set_title "NOP" ;
feedback#set_descr "Does nothing; just for testing." ;
Applicable (fun s -> ["Nop", s])
end
......
......@@ -53,4 +53,3 @@ let main () =
let () = Db.Main.extend main
(*============================================================================*)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment