diff --git a/src/plugins/report/tests/report/no_hyp.ml b/src/plugins/report/tests/report/no_hyp.ml index cb651465511efe31508fe10453ec0bc0f76d1b87..a145963f447e8e630717bf5a0a162627a51bf43f 100644 --- a/src/plugins/report/tests/report/no_hyp.ml +++ b/src/plugins/report/tests/report/no_hyp.ml @@ -1,4 +1,4 @@ -let emitter = +let emitter = Emitter.create "Test" [ Emitter.Property_status ] ~correctness:[] ~tuning:[] let set_status s = @@ -11,7 +11,7 @@ let set_status s = let print_status = Dynamic.get ~plugin:"Report" - "print" + "print" (Datatype.func Datatype.unit Datatype.unit) let clear () = @@ -20,26 +20,36 @@ let clear () = () let main () = - Ast.compute (); - Kernel.feedback "SETTING STATUS TO dont_know"; - set_status Property_status.Dont_know; - print_status (); - Kernel.feedback "SETTING STATUS TO true"; - set_status Property_status.True; - print_status (); + begin + Ast.compute (); + Kernel.feedback "SETTING STATUS TO dont_know"; + set_status Property_status.Dont_know; + print_status (); + Kernel.feedback "SETTING STATUS TO true"; + set_status Property_status.True; + print_status (); + Kernel.feedback "SETTING STATUS TO false_if_reachable"; + set_status Property_status.False_if_reachable; + print_status (); + Kernel.feedback "SETTING STATUS TO dont_know"; + set_status Property_status.Dont_know; + print_status (); + Kernel.feedback "SETTING STATUS TO true"; + set_status Property_status.True; + print_status (); + Kernel.feedback "SETTING STATUS TO false_if_reachable"; + set_status Property_status.False_if_reachable; + print_status (); + (* Kernel.feedback "SETTING STATUS TO false_if_reachable"; (try set_status Property_status.False_if_reachable with Property_status.Inconsistent_emitted_status(s1, s2) -> - Kernel.result "inconsistency between %a and %a" + Kernel.result "inconsistency between %a and %a" Property_status.Emitted_status.pretty s1 Property_status.Emitted_status.pretty s2); Kernel.feedback "CLEARING"; clear (); - Kernel.feedback "SETTING STATUS TO false_if_reachable"; - set_status Property_status.False_if_reachable; - print_status (); - Kernel.feedback "SETTING STATUS TO false_and_reachable"; - set_status Property_status.False_and_reachable; - print_status () + *) + end let () = Db.Main.extend main diff --git a/src/plugins/report/tests/report/oracle/single.1.res.oracle b/src/plugins/report/tests/report/oracle/single.1.res.oracle index a47026150e026717af27c229e66c8b3ff8bd1ae6..088835a7a6788b5f36665493ce3d57f1b512377b 100644 --- a/src/plugins/report/tests/report/oracle/single.1.res.oracle +++ b/src/plugins/report/tests/report/oracle/single.1.res.oracle @@ -32,9 +32,6 @@ 1 Total -------------------------------------------------------------------------------- [kernel] SETTING STATUS TO false_if_reachable -[kernel] inconsistency between **NOT** VALID and VALID -[kernel] CLEARING -[kernel] SETTING STATUS TO false_if_reachable [report] Computing properties status... -------------------------------------------------------------------------------- @@ -51,19 +48,54 @@ 1 Alarm emitted 1 Total -------------------------------------------------------------------------------- -[kernel] SETTING STATUS TO false_and_reachable +[kernel] SETTING STATUS TO dont_know [report] Computing properties status... -------------------------------------------------------------------------------- --- Properties of Function 'main' -------------------------------------------------------------------------------- -[ Bug ] Assertion (file tests/report/single.i, line 9) - by Test. +[ Alarm ] Assertion (file tests/report/single.i, line 9) + By Test, with pending: + - Unreachable program point (file tests/report/single.i, line 9) -------------------------------------------------------------------------------- --- Status Report Summary -------------------------------------------------------------------------------- - 1 Bugs found + 1 Alarm emitted + 1 Total +-------------------------------------------------------------------------------- +[kernel] SETTING STATUS TO true +[report] Computing properties status... + +-------------------------------------------------------------------------------- +--- Properties of Function 'main' +-------------------------------------------------------------------------------- + +[ Alarm ] Assertion (file tests/report/single.i, line 9) + By Test, with pending: + - Unreachable program point (file tests/report/single.i, line 9) + +-------------------------------------------------------------------------------- +--- Status Report Summary +-------------------------------------------------------------------------------- + 1 Alarm emitted + 1 Total +-------------------------------------------------------------------------------- +[kernel] SETTING STATUS TO false_if_reachable +[report] Computing properties status... + +-------------------------------------------------------------------------------- +--- Properties of Function 'main' +-------------------------------------------------------------------------------- + +[ Alarm ] Assertion (file tests/report/single.i, line 9) + By Test, with pending: + - Unreachable program point (file tests/report/single.i, line 9) + +-------------------------------------------------------------------------------- +--- Status Report Summary +-------------------------------------------------------------------------------- + 1 Alarm emitted 1 Total --------------------------------------------------------------------------------