diff --git a/tests/misc/oracle/vis_spec.res.oracle b/tests/misc/oracle/vis_spec.res.oracle index ffe4ed605378cf9506b3fe3b19c6455a6af9f0ee..8151d594e44b27c6cff757e4a8b94291f9d2aa54 100644 --- a/tests/misc/oracle/vis_spec.res.oracle +++ b/tests/misc/oracle/vis_spec.res.oracle @@ -1,8 +1,25 @@ [kernel] Parsing vis_spec.i (no preprocessing) Starting visit -Considering spec of function g -Function prototype; Funspec is 'assigns \nothing;' -Considering spec of function f -Funspec of f is 'assigns \nothing;' through visitor -It is 'assigns \nothing;' through get_spec +Considering vspec of function g +Function prototype; Funspec is +'terminates \true; + exits \false; + allocates \nothing;' +Considering sspec of function f +Funspec of f is '' through visitor +It is 'terminates \true; + exits \false; + assigns \nothing; + allocates \nothing;' +through get_spec +Considering vspec of function f +Funspec of f is 'terminates \true; + exits \false; + allocates \nothing;' +through visitor +It is 'terminates \true; + exits \false; + assigns \nothing; + allocates \nothing;' +through get_spec End visit diff --git a/tests/misc/vis_spec.ml b/tests/misc/vis_spec.ml index dce3f9c206dc50599fd9f2159060d542661e1cb6..19a8ae656851850588a386cfd5640ebaf34f5bdc 100644 --- a/tests/misc/vis_spec.ml +++ b/tests/misc/vis_spec.ml @@ -5,18 +5,27 @@ class pathcrawlerVisitor prj = object(self) inherit Visitor.frama_c_copy prj + method! vfunc fundec = + Format.printf "Considering sspec of function %s@." fundec.svar.vname; + Format.printf "@[Funspec of %s is@ @['%a'@]@ through visitor@]@." + fundec.svar.vname + Printer.pp_funspec fundec.sspec; + Format.printf "@[It is@ @['%a'@]@ through get_spec@]@." + Printer.pp_funspec + (Annotations.funspec (Globals.Functions.get fundec.svar)); + DoChildren + method! vspec sp = - Format.printf "Considering spec of function %s@." + Format.printf "Considering vspec of function %s@." (Kernel_function.get_name (Option.get self#current_kf)); (match self#current_func with - | Some f -> - if f.svar.vname ="f" then ( - Format.printf "@[Funspec of f is@ @['%a'@]@ through visitor@]@." - Printer.pp_funspec sp; - Format.printf "@[It is@ @['%a'@]@ through get_spec@]@." - Printer.pp_funspec - (Annotations.funspec (Globals.Functions.get f.svar)); - ) + | Some fundec -> + Format.printf "@[Funspec of %s is@ @['%a'@]@ through visitor@]@." + fundec.svar.vname + Printer.pp_funspec sp; + Format.printf "@[It is@ @['%a'@]@ through get_spec@]@." + Printer.pp_funspec + (Annotations.funspec (Globals.Functions.get fundec.svar)); | None -> Format.printf "@[Function prototype;@ Funspec is@ @['%a'@]@]@." Printer.pp_funspec sp;