diff --git a/sledge/src/report.ml b/sledge/src/report.ml index f5e135cd0..3a5ae8d28 100644 --- a/sledge/src/report.ml +++ b/sledge/src/report.ml @@ -9,10 +9,8 @@ let unknown_call call = [%Trace.kprintf - (fun _ -> assert false) - "@\n\ - @[%a Called unknown function %a executing instruction@;<1 \ - 2>@[%a@]@]@." + Stop.on_unknown_call + "@\n@[%a Unknown function call %a@;<1 2>@[%a@]@]@." (fun fs call -> Loc.pp fs (Llair.Term.loc call)) call (fun fs (call : Llair.Term.t) -> @@ -25,13 +23,14 @@ let unknown_call call = call Llair.Term.pp call] let invalid_access state pp access loc = - Format.printf "@\n@[%a Invalid memory access@;<1 2>@[%a@]@]@." Loc.pp - (loc access) pp access ; - [%Trace.kprintf - (fun _ -> assert false) - "@\n\ - @[%a Invalid memory access@;<1 2>@[%a@]@;<1 2>@[{ %a@ }@]@]@." - Loc.pp (loc access) pp access State_domain.pp state] + let rep fs = + Format.fprintf fs "%a Invalid memory access@;<1 2>@[%a@]" Loc.pp + (loc access) pp access + in + Format.printf "@\n@[%t@]@." rep ; + [%Trace.printf + "@\n@[%t@;<1 2>@[{ %a@ }@]@]@." rep State_domain.pp state] ; + Stop.on_invalid_access () let invalid_access_inst state inst = invalid_access state Llair.Inst.pp inst Llair.Inst.loc diff --git a/sledge/src/stop.ml b/sledge/src/stop.ml new file mode 100644 index 000000000..db4f3377c --- /dev/null +++ b/sledge/src/stop.ml @@ -0,0 +1,11 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +(** Stop analysis when encountering issues *) + +let on_unknown_call _ = [%Trace.kprintf (fun _ -> assert false) ""] +let on_invalid_access _ = [%Trace.kprintf (fun _ -> assert false) ""] diff --git a/sledge/src/stop.mli b/sledge/src/stop.mli new file mode 100644 index 000000000..6f9b4e6c6 --- /dev/null +++ b/sledge/src/stop.mli @@ -0,0 +1,11 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +(** Stop analysis when encountering issues *) + +val on_unknown_call : 'a -> unit +val on_invalid_access : 'a -> unit