From 86c2294097a64058da9dc727fd245df754a6eed9 Mon Sep 17 00:00:00 2001 From: S41d Date: Wed, 28 May 2025 16:12:37 +0200 Subject: [PATCH 1/4] model with entry point: generation --- src/bin/owi.ml | 18 ++++++++++++++++-- src/cmd/cmd_c.ml | 5 +++-- src/cmd/cmd_c.mli | 1 + src/cmd/cmd_conc.ml | 2 +- src/cmd/cmd_conc.mli | 1 + src/cmd/cmd_cpp.ml | 3 ++- src/cmd/cmd_cpp.mli | 1 + src/cmd/cmd_iso.ml | 2 +- src/cmd/cmd_rust.ml | 3 ++- src/cmd/cmd_rust.mli | 1 + src/cmd/cmd_sym.ml | 43 ++++++++++++++++++++++++++++++++----------- src/cmd/cmd_sym.mli | 3 +++ src/cmd/cmd_zig.ml | 3 ++- 13 files changed, 66 insertions(+), 20 deletions(-) diff --git a/src/bin/owi.ml b/src/bin/owi.ml index c7f7a87de..93b55a142 100644 --- a/src/bin/owi.ml +++ b/src/bin/owi.ml @@ -150,6 +150,10 @@ let model_out_file = & opt (some path_conv) None & info [ "model-out-file" ] ~docv:"FILE" ~doc ) +let model_with_entry_point = + let doc = "Add the entry point in the generated model for easier replay." in + Arg.(value & flag & info [ "model-with-entry-point" ] ~doc) + let rac = let doc = "runtime assertion checking mode" in Arg.(value & flag & info [ "rac" ] ~doc) @@ -247,12 +251,14 @@ let c_cmd = and+ out_file and+ model_out_file and+ with_breadcrumbs + and+ model_with_entry_point and+ entry_point in Cmd_c.cmd ~arch ~property ~testcomp ~workspace ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~eacsl ~solver ~model_format ~entry_point ~invoke_with_symbols ~out_file ~model_out_file ~with_breadcrumbs + ~model_with_entry_point (* owi cpp *) let cpp_info = @@ -284,12 +290,13 @@ let cpp_cmd = and+ workspace and+ model_out_file and+ with_breadcrumbs + and+ model_with_entry_point and+ entry_point in Cmd_cpp.cmd ~arch ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format ~entry_point ~invoke_with_symbols ~out_file ~workspace ~model_out_file - ~with_breadcrumbs + ~with_breadcrumbs ~model_with_entry_point (* owi conc *) @@ -317,11 +324,13 @@ let conc_cmd = and+ model_out_file and+ invoke_with_symbols and+ with_breadcrumbs + and+ model_with_entry_point and+ entry_point in Cmd_conc.cmd ~unsafe ~rac ~srac ~optimize ~workers ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point ~invoke_with_symbols ~model_out_file ~with_breadcrumbs + ~model_with_entry_point (* owi fmt *) @@ -475,12 +484,13 @@ let rust_cmd = and+ workspace and+ model_out_file and+ with_breadcrumbs + and+ model_with_entry_point and+ entry_point in Cmd_rust.cmd ~arch ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format ~entry_point ~invoke_with_symbols ~out_file ~workspace ~model_out_file - ~with_breadcrumbs + ~with_breadcrumbs ~model_with_entry_point (* owi script *) @@ -525,11 +535,13 @@ let sym_cmd = and+ entry_point and+ model_out_file and+ with_breadcrumbs + and+ model_with_entry_point and+ invoke_with_symbols in Cmd_sym.cmd ~unsafe ~rac ~srac ~optimize ~workers ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point ~invoke_with_symbols ~model_out_file ~with_breadcrumbs + ~model_with_entry_point (* owi validate *) @@ -619,11 +631,13 @@ let zig_cmd = and+ model_out_file and+ () = setup_log and+ with_breadcrumbs + and+ model_with_entry_point and+ entry_point in Cmd_zig.cmd ~includes ~workers ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format ~entry_point ~invoke_with_symbols ~out_file ~workspace ~model_out_file ~with_breadcrumbs + ~model_with_entry_point (* owi *) diff --git a/src/cmd/cmd_c.ml b/src/cmd/cmd_c.ml index 52d50ca8f..1cca934bf 100644 --- a/src/cmd/cmd_c.ml +++ b/src/cmd/cmd_c.ml @@ -177,8 +177,8 @@ let cmd ~arch ~property ~testcomp:_ ~workspace ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~eacsl ~solver ~model_format ~(entry_point : string option) - ~invoke_with_symbols ~out_file ~model_out_file ~with_breadcrumbs : - unit Result.t = + ~invoke_with_symbols ~out_file ~model_out_file ~with_breadcrumbs + ~model_with_entry_point : unit Result.t = let* workspace = match workspace with | Some path -> Ok path @@ -201,3 +201,4 @@ let cmd ~arch ~property ~testcomp:_ ~workspace ~workers ~opt_lvl ~includes ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point ~invoke_with_symbols ~model_out_file ~with_breadcrumbs + ~model_with_entry_point diff --git a/src/cmd/cmd_c.mli b/src/cmd/cmd_c.mli index a8416afcf..2ca3fe926 100644 --- a/src/cmd/cmd_c.mli +++ b/src/cmd/cmd_c.mli @@ -27,4 +27,5 @@ val cmd : -> out_file:Fpath.t option -> model_out_file:Fpath.t option -> with_breadcrumbs:bool + -> model_with_entry_point:bool -> unit Result.t diff --git a/src/cmd/cmd_conc.ml b/src/cmd/cmd_conc.ml index b25dccc79..602fd87f0 100644 --- a/src/cmd/cmd_conc.ml +++ b/src/cmd/cmd_conc.ml @@ -433,7 +433,7 @@ let assignments_to_model (assignments : (Smtml.Symbol.t * V.t) list) : let cmd ~unsafe ~rac ~srac ~optimize ~workers:_ ~no_stop_at_failure:_ ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order:_ ~fail_mode:_ ~workspace ~solver ~files ~model_format ~entry_point - ~invoke_with_symbols ~model_out_file ~with_breadcrumbs:_ = + ~invoke_with_symbols ~model_out_file ~with_breadcrumbs:_ ~model_with_entry_point:_ = let* workspace = match workspace with | Some path -> Ok path diff --git a/src/cmd/cmd_conc.mli b/src/cmd/cmd_conc.mli index 67cb88c98..3336824da 100644 --- a/src/cmd/cmd_conc.mli +++ b/src/cmd/cmd_conc.mli @@ -21,4 +21,5 @@ val cmd : -> invoke_with_symbols:bool -> model_out_file:Fpath.t option -> with_breadcrumbs:bool + -> model_with_entry_point:bool -> unit Result.t diff --git a/src/cmd/cmd_cpp.ml b/src/cmd/cmd_cpp.ml index 367c83ea5..0ddcd0016 100644 --- a/src/cmd/cmd_cpp.ml +++ b/src/cmd/cmd_cpp.ml @@ -103,7 +103,7 @@ let cmd ~arch:_ ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format ~entry_point ~invoke_with_symbols ~out_file ~workspace ~model_out_file - ~with_breadcrumbs : unit Result.t = + ~with_breadcrumbs ~model_with_entry_point : unit Result.t = let* workspace = match workspace with | Some path -> Ok path @@ -124,3 +124,4 @@ let cmd ~arch:_ ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point ~invoke_with_symbols ~model_out_file ~with_breadcrumbs + ~model_with_entry_point diff --git a/src/cmd/cmd_cpp.mli b/src/cmd/cmd_cpp.mli index 9639480b5..8d9f6182a 100644 --- a/src/cmd/cmd_cpp.mli +++ b/src/cmd/cmd_cpp.mli @@ -24,4 +24,5 @@ val cmd : -> workspace:Fpath.t option -> model_out_file:Fpath.t option -> with_breadcrumbs:bool + -> model_with_entry_point:bool -> unit Result.t diff --git a/src/cmd/cmd_iso.ml b/src/cmd/cmd_iso.ml index e1fcfebe6..c3dc64f7a 100644 --- a/src/cmd/cmd_iso.ml +++ b/src/cmd/cmd_iso.ml @@ -443,5 +443,5 @@ let cmd ~deterministic_result_order ~fail_mode ~files ~model_format Cmd_sym.handle_result ~fail_mode ~workers ~solver ~deterministic_result_order ~model_format ~no_value ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure - ~model_out_file ~with_breadcrumbs result ) + ~model_out_file ~with_breadcrumbs ~model_with_entry_point:false ~entry_point:None result ) () common_exports diff --git a/src/cmd/cmd_rust.ml b/src/cmd/cmd_rust.ml index 5752d9379..c7e9a82b7 100644 --- a/src/cmd/cmd_rust.ml +++ b/src/cmd/cmd_rust.ml @@ -50,7 +50,7 @@ let cmd ~arch:_ ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format ~entry_point ~invoke_with_symbols ~out_file ~(workspace : Fpath.t option) - ~model_out_file ~with_breadcrumbs : unit Result.t = + ~model_out_file ~with_breadcrumbs ~model_with_entry_point : unit Result.t = let* workspace = match workspace with | Some path -> Ok path @@ -68,3 +68,4 @@ let cmd ~arch:_ ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point ~invoke_with_symbols ~model_out_file ~with_breadcrumbs + ~model_with_entry_point diff --git a/src/cmd/cmd_rust.mli b/src/cmd/cmd_rust.mli index 9639480b5..8d9f6182a 100644 --- a/src/cmd/cmd_rust.mli +++ b/src/cmd/cmd_rust.mli @@ -24,4 +24,5 @@ val cmd : -> workspace:Fpath.t option -> model_out_file:Fpath.t option -> with_breadcrumbs:bool + -> model_with_entry_point:bool -> unit Result.t diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml index 48eca3bb5..fad5dee23 100644 --- a/src/cmd/cmd_sym.ml +++ b/src/cmd/cmd_sym.ml @@ -34,7 +34,8 @@ let run_file ~entry_point ~unsafe ~rac ~srac ~optimize ~invoke_with_symbols _pc Interpret.Symbolic.modul link_state.envs m let print_bug ~model_format ~model_out_file ~id ~no_value ~no_stop_at_failure - ~no_assert_failure_expression_printing ~with_breadcrumbs bug = + ~no_assert_failure_expression_printing ~with_breadcrumbs + ~model_with_entry_point ~entry_point bug = let pp fmt (model, labels, breadcrumbs, scoped_values) = match model_format with | Cmd_utils.Json -> @@ -62,7 +63,8 @@ let print_bug ~model_format ~model_out_file ~id ~no_value ~no_stop_at_failure } ) labels in - let children = + let model = { model with children = model.children @ lbls } in + let model = if with_breadcrumbs then let bcrumbs = [ { Scfg.Types.name = "breadcrumbs" @@ -71,10 +73,22 @@ let print_bug ~model_format ~model_out_file ~id ~no_value ~no_stop_at_failure } ] in - model.children @ lbls @ bcrumbs - else model.children @ lbls + { model with children = model.children @ bcrumbs } + else model in - Scfg.Pp.directive fmt { model with children } + let model = + if model_with_entry_point then + let ep = + [ { Scfg.Types.name = "entry_point" + ; params = [ entry_point ] + ; children = [] + } + ] + in + { model with children = model.children @ ep } + else model + in + Scfg.Pp.directive fmt model in let to_file path model labels breadcrumbs symbol_scopes = let model_ext = match model_format with Json -> "json" | Scfg -> "scfg" in @@ -117,7 +131,7 @@ let print_bug ~model_format ~model_out_file ~id ~no_value ~no_stop_at_failure let print_and_count_failures ~model_format ~model_out_file ~no_value ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure - ~count_acc ~results ~with_breadcrumbs = + ~count_acc ~results ~with_breadcrumbs ~model_with_entry_point ~entry_point = let test_suite_dir = Fpath.(workspace / "test-suite") in let* (_created : bool) = if not no_value then OS.Dir.create test_suite_dir else Ok false @@ -133,7 +147,7 @@ let print_and_count_failures ~model_format ~model_out_file ~no_value let* () = print_bug ~model_format ~model_out_file ~id:count_acc ~no_value ~no_stop_at_failure ~no_assert_failure_expression_printing - ~with_breadcrumbs bug + ~with_breadcrumbs ~model_with_entry_point ~entry_point bug in Ok model | `Error e -> Error e @@ -162,7 +176,7 @@ let sort_results deterministic_result_order results = let handle_result ~workers ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~workspace ~solver ~model_format ~model_out_file ~with_breadcrumbs - (result : unit Symbolic.Choice.t) = + ~model_with_entry_point ~entry_point (result : unit Symbolic.Choice.t) = let thread = Thread_with_memory.init () in let res_queue = Wq.make () in let path_count = Atomic.make 0 in @@ -193,10 +207,16 @@ let handle_result ~workers ~no_stop_at_failure ~no_value Array.iter Domain.join join_handles ) in let results = sort_results deterministic_result_order results in + let* entry_point = + if model_with_entry_point then + match entry_point with Some ep -> Ok ep | None -> Fmt.error_msg "" + else Ok "" + in let* count = print_and_count_failures ~model_format ~model_out_file ~no_value ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure - ~count_acc:0 ~results ~with_breadcrumbs + ~count_acc:0 ~results ~with_breadcrumbs ~model_with_entry_point + ~entry_point in Logs.info (fun m -> m "Completed paths: %d" (Atomic.get path_count)); let+ () = if count > 0 then Error (`Found_bug count) else Ok () in @@ -209,7 +229,7 @@ let handle_result ~workers ~no_stop_at_failure ~no_value let cmd ~unsafe ~rac ~srac ~optimize ~workers ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point ~invoke_with_symbols - ~model_out_file ~with_breadcrumbs = + ~model_out_file ~with_breadcrumbs ~model_with_entry_point = let* workspace = match workspace with | Some path -> Ok path @@ -226,4 +246,5 @@ let cmd ~unsafe ~rac ~srac ~optimize ~workers ~no_stop_at_failure ~no_value in handle_result ~fail_mode ~workers ~solver ~deterministic_result_order ~model_format ~no_value ~no_assert_failure_expression_printing ~workspace - ~no_stop_at_failure ~model_out_file ~with_breadcrumbs result + ~no_stop_at_failure ~model_out_file ~with_breadcrumbs + ~model_with_entry_point ~entry_point result diff --git a/src/cmd/cmd_sym.mli b/src/cmd/cmd_sym.mli index 139bb5445..cb43e2351 100644 --- a/src/cmd/cmd_sym.mli +++ b/src/cmd/cmd_sym.mli @@ -23,6 +23,8 @@ val handle_result : -> model_format:Cmd_utils.model_format -> model_out_file:Fpath.t option -> with_breadcrumbs:bool + -> model_with_entry_point:bool + -> entry_point:string option -> unit Symbolic.Choice.t -> unit Result.t @@ -45,4 +47,5 @@ val cmd : -> invoke_with_symbols:bool -> model_out_file:Fpath.t option -> with_breadcrumbs:bool + -> model_with_entry_point:bool -> unit Result.t diff --git a/src/cmd/cmd_zig.ml b/src/cmd/cmd_zig.ml index 256b487c7..439cc56d8 100644 --- a/src/cmd/cmd_zig.ml +++ b/src/cmd/cmd_zig.ml @@ -61,7 +61,7 @@ let compile ~workspace ~entry_point ~includes ~out_file (files : Fpath.t list) : let cmd ~workers ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format ~entry_point ~invoke_with_symbols - ~out_file ~workspace ~model_out_file ~with_breadcrumbs : unit Result.t = + ~out_file ~workspace ~model_out_file ~with_breadcrumbs ~model_with_entry_point : unit Result.t = let* workspace = match workspace with | Some path -> Ok path @@ -85,3 +85,4 @@ let cmd ~workers ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point ~invoke_with_symbols ~model_out_file ~with_breadcrumbs + ~model_with_entry_point From f6ddbcbadd3c03fbdd2179389f44308d23b88ea2 Mon Sep 17 00:00:00 2001 From: S41d Date: Fri, 30 May 2025 18:01:19 +0200 Subject: [PATCH 2/4] model with entry point: replay --- doc/src/manpages/owi-c.md | 3 +++ doc/src/manpages/owi-conc.md | 3 +++ doc/src/manpages/owi-cpp.md | 3 +++ doc/src/manpages/owi-rust.md | 3 +++ doc/src/manpages/owi-sym.md | 3 +++ doc/src/manpages/owi-zig.md | 3 +++ src/cmd/cmd_replay.ml | 17 +++++++++++------ src/symbolic/symbol_scope.ml | 11 +++++++++-- src/symbolic/symbol_scope.mli | 4 ++-- test/c/dune | 1 + test/c/invoke_with_symbols.t | 7 +++++-- test/c/model_with_entry_point.c | 17 +++++++++++++++++ test/c/model_with_entry_point.t | 25 +++++++++++++++++++++++++ 13 files changed, 88 insertions(+), 12 deletions(-) create mode 100644 test/c/model_with_entry_point.c create mode 100644 test/c/model_with_entry_point.t diff --git a/doc/src/manpages/owi-c.md b/doc/src/manpages/owi-c.md index 695d2940a..ec869fa5f 100644 --- a/doc/src/manpages/owi-c.md +++ b/doc/src/manpages/owi-c.md @@ -56,6 +56,9 @@ OPTIONS given this is used as a prefix and the ouputed files would have PREFIX_%d. + --model-with-entry-point + Add the entry point in the generated model for easier replay. + --no-assert-failure-expression-printing do not display the expression in the assert failure diff --git a/doc/src/manpages/owi-conc.md b/doc/src/manpages/owi-conc.md index 1f3344ec3..79cd7f9ef 100644 --- a/doc/src/manpages/owi-conc.md +++ b/doc/src/manpages/owi-conc.md @@ -41,6 +41,9 @@ OPTIONS given this is used as a prefix and the ouputed files would have PREFIX_%d. + --model-with-entry-point + Add the entry point in the generated model for easier replay. + --no-assert-failure-expression-printing do not display the expression in the assert failure diff --git a/doc/src/manpages/owi-cpp.md b/doc/src/manpages/owi-cpp.md index e3a9c87bb..29aeb6954 100644 --- a/doc/src/manpages/owi-cpp.md +++ b/doc/src/manpages/owi-cpp.md @@ -51,6 +51,9 @@ OPTIONS given this is used as a prefix and the ouputed files would have PREFIX_%d. + --model-with-entry-point + Add the entry point in the generated model for easier replay. + --no-assert-failure-expression-printing do not display the expression in the assert failure diff --git a/doc/src/manpages/owi-rust.md b/doc/src/manpages/owi-rust.md index 4ee012d8c..6193c9ace 100644 --- a/doc/src/manpages/owi-rust.md +++ b/doc/src/manpages/owi-rust.md @@ -51,6 +51,9 @@ OPTIONS given this is used as a prefix and the ouputed files would have PREFIX_%d. + --model-with-entry-point + Add the entry point in the generated model for easier replay. + --no-assert-failure-expression-printing do not display the expression in the assert failure diff --git a/doc/src/manpages/owi-sym.md b/doc/src/manpages/owi-sym.md index e7220d99a..cc74ae3eb 100644 --- a/doc/src/manpages/owi-sym.md +++ b/doc/src/manpages/owi-sym.md @@ -41,6 +41,9 @@ OPTIONS given this is used as a prefix and the ouputed files would have PREFIX_%d. + --model-with-entry-point + Add the entry point in the generated model for easier replay. + --no-assert-failure-expression-printing do not display the expression in the assert failure diff --git a/doc/src/manpages/owi-zig.md b/doc/src/manpages/owi-zig.md index cb263afa5..e0bcbe327 100644 --- a/doc/src/manpages/owi-zig.md +++ b/doc/src/manpages/owi-zig.md @@ -48,6 +48,9 @@ OPTIONS given this is used as a prefix and the ouputed files would have PREFIX_%d. + --model-with-entry-point + Add the entry point in the generated model for easier replay. + --no-assert-failure-expression-printing do not display the expression in the assert failure diff --git a/src/cmd/cmd_replay.ml b/src/cmd/cmd_replay.ml index 6736efbd7..e5b617f31 100644 --- a/src/cmd/cmd_replay.ml +++ b/src/cmd/cmd_replay.ml @@ -261,19 +261,19 @@ let run_file ~unsafe ~optimize ~entry_point ~invoke_with_symbols filename model let cmd ~unsafe ~optimize ~replay_file ~source_file ~entry_point ~invoke_with_symbols = + let file_ext = Fpath.get_ext replay_file in let* parse_fn = - let ext = Fpath.get_ext replay_file in - match String.lowercase_ascii ext with + match String.lowercase_ascii file_ext with | ".json" -> Ok Symbol_scope.model_of_json | ".scfg" -> Ok Symbol_scope.model_of_scfg - | _ -> Error (`Unsupported_file_extension ext) + | _ -> Error (`Unsupported_file_extension file_ext) in let* file_content = Bos.OS.File.read replay_file in - let* model = + let* model_entry_point, model = match parse_fn file_content with | Error (`Msg msg) -> Error (`Invalid_model msg) | Error err -> Error err - | Ok model -> + | Ok (entry_point, model) -> let bindings = Smtml.Model.get_bindings model in let+ model = list_map @@ -298,8 +298,13 @@ let cmd ~unsafe ~optimize ~replay_file ~source_file ~entry_point (Fmt.str "unexpected value type: %a" Smtml.Value.pp v) ) ) bindings in - Array.of_list model + (entry_point, Array.of_list model) in + let entry_point = + if Option.is_none entry_point then model_entry_point else entry_point + in + Logs.debug (fun m -> m "%s" (Option.value ~default:"na" entry_point)); + Logs.debug (fun m -> m "%s" (Option.value ~default:"na" model_entry_point)); let+ () = run_file ~unsafe ~optimize ~entry_point ~invoke_with_symbols source_file model diff --git a/src/symbolic/symbol_scope.ml b/src/symbolic/symbol_scope.ml index 18985b086..475ba471d 100644 --- a/src/symbolic/symbol_scope.ml +++ b/src/symbolic/symbol_scope.ml @@ -204,7 +204,10 @@ let model_of_json json_str = match List.assoc_opt "model" root with | Some items -> let+ () = process_json (Util.to_list items) in - tbl + let entry_point = + Option.map Util.to_string (List.assoc_opt "entry_point" root) + in + (entry_point, tbl) | None -> Fmt.error_msg "JSON does not contain model field" ) | _ -> Fmt.error_msg "Invalid JSON format for symbol scope:@. %a" @@ -238,6 +241,10 @@ let model_of_scfg scfg = match Query.get_dir "model" scfg with | Some model -> let+ () = process_dirs model.children in - tbl + let entry_point = + let dir = Query.get_dir "entry_point" model.children in + Option.bind dir (fun dir -> Result.to_option @@ Query.get_param 0 dir) + in + (entry_point, tbl) | None -> Fmt.error_msg "Could not find the directive `model` in the scfg config" diff --git a/src/symbolic/symbol_scope.mli b/src/symbolic/symbol_scope.mli index c0a2c21f5..afcb27c72 100644 --- a/src/symbolic/symbol_scope.mli +++ b/src/symbolic/symbol_scope.mli @@ -24,6 +24,6 @@ val to_json : -> t -> [> `Assoc of (string * Yojson.Basic.t) list ] -val model_of_json : string -> Smtml.Model.t Result.t +val model_of_json : string -> (string option * Smtml.Model.t) Result.t -val model_of_scfg : string -> Smtml.Model.t Result.t +val model_of_scfg : string -> (string option * Smtml.Model.t) Result.t diff --git a/test/c/dune b/test/c/dune index 4efc03a53..9cdf4d354 100644 --- a/test/c/dune +++ b/test/c/dune @@ -15,6 +15,7 @@ main.c malloc_aligned.c malloc_zero.c + model_with_entry_point.c multi_model.c range.c scopes.c)) diff --git a/test/c/invoke_with_symbols.t b/test/c/invoke_with_symbols.t index 903842498..c31f44d7e 100644 --- a/test/c/invoke_with_symbols.t +++ b/test/c/invoke_with_symbols.t @@ -1,5 +1,8 @@ - $ owi c --entry-point=f --invoke-with-symbols ./invoke_with_symbols.c - owi: [ERROR] Assert failure: (f32.ne (f32.convert_i32_s symbol_0) symbol_2) + $ owi c -O0 --entry-point=f --invoke-with-symbols ./invoke_with_symbols.c + owi: [ERROR] Assert failure: (f32.ne + (f32.reinterpret_int + (i32.reinterpret_float symbol_2)) + (f32.convert_i32_s symbol_0)) model { symbol symbol_0 i32 1 symbol symbol_1 i64 0 diff --git a/test/c/model_with_entry_point.c b/test/c/model_with_entry_point.c new file mode 100644 index 000000000..9a4cad08b --- /dev/null +++ b/test/c/model_with_entry_point.c @@ -0,0 +1,17 @@ +#include + +int fun() { + int i = owi_i32(); + owi_assume(i < 2); + owi_assume(i > 0); + owi_assert(i == 2); + return i; +} + +int main() { + int i = owi_i32(); + owi_assume(i < 3); + owi_assume(i > 1); + owi_assert(i == 3); + return i; +} diff --git a/test/c/model_with_entry_point.t b/test/c/model_with_entry_point.t new file mode 100644 index 000000000..d3760a555 --- /dev/null +++ b/test/c/model_with_entry_point.t @@ -0,0 +1,25 @@ + $ owi c model_with_entry_point.c --model-with-entry-point -O0 --entry-point=main + owi: [ERROR] Assert failure: (bool.eq symbol_0 3) + model { + symbol symbol_0 i32 2 + entry_point main + } + owi: [ERROR] Reached problem! + [13] + + $ owi c model_with_entry_point.c --model-with-entry-point -O0 --entry-point=fun + owi: [ERROR] Assert failure: (bool.eq symbol_0 2) + model { + symbol symbol_0 i32 1 + entry_point fun + } + owi: [ERROR] Reached problem! + [13] + + $ owi c model_with_entry_point.c --model-with-entry-point -O0 --entry-point=fun --model-out-file=output.scfg -o output.wasm + owi: [ERROR] Assert failure: (bool.eq symbol_0 2) + owi: [ERROR] Reached problem! + [13] + + $ owi replay output.wasm --replay-file=output.scfg + Assertion failure was correctly reached! From f45fee9bfb54de11216d5e27ce4531b5e590f555 Mon Sep 17 00:00:00 2001 From: S41d Date: Fri, 30 May 2025 18:04:51 +0200 Subject: [PATCH 3/4] changes.md and fmt --- CHANGES.md | 1 + src/cmd/cmd_conc.ml | 3 ++- src/cmd/cmd_iso.ml | 3 ++- src/cmd/cmd_zig.ml | 3 ++- 4 files changed, 7 insertions(+), 3 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 1dfcee3e6..1a2bc512b 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -41,6 +41,7 @@ - add `owi_label_is_covered` primitive - add scopes with `owi_open_scope` and `owi_close_scope` primitives - start support for simd instructions +- add `--model-with-entry-point` option ## 0.2 - 2024-04-24 diff --git a/src/cmd/cmd_conc.ml b/src/cmd/cmd_conc.ml index 602fd87f0..4c4ba7cbc 100644 --- a/src/cmd/cmd_conc.ml +++ b/src/cmd/cmd_conc.ml @@ -433,7 +433,8 @@ let assignments_to_model (assignments : (Smtml.Symbol.t * V.t) list) : let cmd ~unsafe ~rac ~srac ~optimize ~workers:_ ~no_stop_at_failure:_ ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order:_ ~fail_mode:_ ~workspace ~solver ~files ~model_format ~entry_point - ~invoke_with_symbols ~model_out_file ~with_breadcrumbs:_ ~model_with_entry_point:_ = + ~invoke_with_symbols ~model_out_file ~with_breadcrumbs:_ + ~model_with_entry_point:_ = let* workspace = match workspace with | Some path -> Ok path diff --git a/src/cmd/cmd_iso.ml b/src/cmd/cmd_iso.ml index c3dc64f7a..2ea3fe194 100644 --- a/src/cmd/cmd_iso.ml +++ b/src/cmd/cmd_iso.ml @@ -443,5 +443,6 @@ let cmd ~deterministic_result_order ~fail_mode ~files ~model_format Cmd_sym.handle_result ~fail_mode ~workers ~solver ~deterministic_result_order ~model_format ~no_value ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure - ~model_out_file ~with_breadcrumbs ~model_with_entry_point:false ~entry_point:None result ) + ~model_out_file ~with_breadcrumbs ~model_with_entry_point:false + ~entry_point:None result ) () common_exports diff --git a/src/cmd/cmd_zig.ml b/src/cmd/cmd_zig.ml index 439cc56d8..f6552e839 100644 --- a/src/cmd/cmd_zig.ml +++ b/src/cmd/cmd_zig.ml @@ -61,7 +61,8 @@ let compile ~workspace ~entry_point ~includes ~out_file (files : Fpath.t list) : let cmd ~workers ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format ~entry_point ~invoke_with_symbols - ~out_file ~workspace ~model_out_file ~with_breadcrumbs ~model_with_entry_point : unit Result.t = + ~out_file ~workspace ~model_out_file ~with_breadcrumbs ~model_with_entry_point + : unit Result.t = let* workspace = match workspace with | Some path -> Ok path From 324755c5f37de229cb543a7229185feab53e09d0 Mon Sep 17 00:00:00 2001 From: S41d Date: Mon, 2 Jun 2025 11:41:02 +0200 Subject: [PATCH 4/4] set as default behavoir --- CHANGES.md | 2 +- doc/src/manpages/owi-c.md | 3 --- doc/src/manpages/owi-conc.md | 3 --- doc/src/manpages/owi-cpp.md | 3 --- doc/src/manpages/owi-rust.md | 3 --- doc/src/manpages/owi-sym.md | 3 --- doc/src/manpages/owi-zig.md | 3 --- doc/src/symex/quickstart/cpp.md | 1 + doc/src/symex/quickstart/rust.md | 1 + doc/src/symex/quickstart/zig.md | 1 + doc/src/symex/sap/examples.md | 6 +++++ doc/src/symex/verification/eacsl.md | 1 + src/bin/owi.ml | 18 ++------------- src/cmd/cmd_c.ml | 5 ++--- src/cmd/cmd_c.mli | 1 - src/cmd/cmd_conc.ml | 3 +-- src/cmd/cmd_conc.mli | 1 - src/cmd/cmd_cpp.ml | 3 +-- src/cmd/cmd_cpp.mli | 1 - src/cmd/cmd_iso.ml | 3 +-- src/cmd/cmd_replay.ml | 7 ++++-- src/cmd/cmd_rust.ml | 3 +-- src/cmd/cmd_rust.mli | 1 - src/cmd/cmd_sym.ml | 27 +++++++++-------------- src/cmd/cmd_sym.mli | 2 -- src/cmd/cmd_zig.ml | 4 +--- test/c/collections-c/tests_array.t | 1 + test/c/collections-c/tests_buggy.t | 2 ++ test/c/collections-c/tests_pqueue.t | 2 ++ test/c/double_free.t | 4 +++- test/c/eacsl/function/integer_dividable.t | 1 + test/c/eacsl/function/max.t | 1 + test/c/eacsl/function/max_ptr.t | 1 + test/c/eacsl/ghost/case.t | 1 + test/c/eacsl/ghost/default.t | 1 + test/c/eacsl/ghost/else.t | 1 + test/c/eacsl/ghost/global.t | 1 + test/c/entry_point.t | 1 + test/c/exit.t | 1 + test/c/invisible_bool.t | 1 + test/c/invoke_with_symbols.t | 1 + test/c/label.t | 2 ++ test/c/main.t | 1 + test/c/malloc_zero.t | 8 +++++-- test/c/model_with_entry_point.t | 6 ++--- test/c/range.t | 1 + test/c/scopes.t | 1 + test/c/test-comp/simple.t | 1 + test/cpp/entry_point.t | 1 + test/replay/alloc.t | 1 + test/rust/entry_point.t | 1 + test/sym/entry_points/export.t | 1 + test/sym/print_pc.t | 1 + test/zig/entry_point.t | 1 + 54 files changed, 75 insertions(+), 80 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 1a2bc512b..35ecdc3af 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -41,7 +41,7 @@ - add `owi_label_is_covered` primitive - add scopes with `owi_open_scope` and `owi_close_scope` primitives - start support for simd instructions -- add `--model-with-entry-point` option +- add the symbolic execution's entry point to the model ## 0.2 - 2024-04-24 diff --git a/doc/src/manpages/owi-c.md b/doc/src/manpages/owi-c.md index ec869fa5f..695d2940a 100644 --- a/doc/src/manpages/owi-c.md +++ b/doc/src/manpages/owi-c.md @@ -56,9 +56,6 @@ OPTIONS given this is used as a prefix and the ouputed files would have PREFIX_%d. - --model-with-entry-point - Add the entry point in the generated model for easier replay. - --no-assert-failure-expression-printing do not display the expression in the assert failure diff --git a/doc/src/manpages/owi-conc.md b/doc/src/manpages/owi-conc.md index 79cd7f9ef..1f3344ec3 100644 --- a/doc/src/manpages/owi-conc.md +++ b/doc/src/manpages/owi-conc.md @@ -41,9 +41,6 @@ OPTIONS given this is used as a prefix and the ouputed files would have PREFIX_%d. - --model-with-entry-point - Add the entry point in the generated model for easier replay. - --no-assert-failure-expression-printing do not display the expression in the assert failure diff --git a/doc/src/manpages/owi-cpp.md b/doc/src/manpages/owi-cpp.md index 29aeb6954..e3a9c87bb 100644 --- a/doc/src/manpages/owi-cpp.md +++ b/doc/src/manpages/owi-cpp.md @@ -51,9 +51,6 @@ OPTIONS given this is used as a prefix and the ouputed files would have PREFIX_%d. - --model-with-entry-point - Add the entry point in the generated model for easier replay. - --no-assert-failure-expression-printing do not display the expression in the assert failure diff --git a/doc/src/manpages/owi-rust.md b/doc/src/manpages/owi-rust.md index 6193c9ace..4ee012d8c 100644 --- a/doc/src/manpages/owi-rust.md +++ b/doc/src/manpages/owi-rust.md @@ -51,9 +51,6 @@ OPTIONS given this is used as a prefix and the ouputed files would have PREFIX_%d. - --model-with-entry-point - Add the entry point in the generated model for easier replay. - --no-assert-failure-expression-printing do not display the expression in the assert failure diff --git a/doc/src/manpages/owi-sym.md b/doc/src/manpages/owi-sym.md index cc74ae3eb..e7220d99a 100644 --- a/doc/src/manpages/owi-sym.md +++ b/doc/src/manpages/owi-sym.md @@ -41,9 +41,6 @@ OPTIONS given this is used as a prefix and the ouputed files would have PREFIX_%d. - --model-with-entry-point - Add the entry point in the generated model for easier replay. - --no-assert-failure-expression-printing do not display the expression in the assert failure diff --git a/doc/src/manpages/owi-zig.md b/doc/src/manpages/owi-zig.md index e0bcbe327..cb263afa5 100644 --- a/doc/src/manpages/owi-zig.md +++ b/doc/src/manpages/owi-zig.md @@ -48,9 +48,6 @@ OPTIONS given this is used as a prefix and the ouputed files would have PREFIX_%d. - --model-with-entry-point - Add the entry point in the generated model for easier replay. - --no-assert-failure-expression-printing do not display the expression in the assert failure diff --git a/doc/src/symex/quickstart/cpp.md b/doc/src/symex/quickstart/cpp.md index fce86e683..25cbc895a 100644 --- a/doc/src/symex/quickstart/cpp.md +++ b/doc/src/symex/quickstart/cpp.md @@ -24,6 +24,7 @@ owi: [ERROR] Assert failure model { symbol symbol_0 i32 -2147483648 symbol symbol_1 i32 -2147483646 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/doc/src/symex/quickstart/rust.md b/doc/src/symex/quickstart/rust.md index b0e48cad8..b0e5235a0 100644 --- a/doc/src/symex/quickstart/rust.md +++ b/doc/src/symex/quickstart/rust.md @@ -29,6 +29,7 @@ owi: [ERROR] Assert failure model { symbol symbol_0 i32 -487586839 symbol symbol_1 i32 486539486 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/doc/src/symex/quickstart/zig.md b/doc/src/symex/quickstart/zig.md index 3c4e09b26..1d89f3dca 100644 --- a/doc/src/symex/quickstart/zig.md +++ b/doc/src/symex/quickstart/zig.md @@ -35,6 +35,7 @@ $ owi zig ./fib.zig -w1 --no-assert-failure-expression-printing owi: [ERROR] Assert failure model { symbol symbol_0 i32 7 + entry_point _start } owi: [ERROR] Reached problem! [13] diff --git a/doc/src/symex/sap/examples.md b/doc/src/symex/sap/examples.md index ca3c4fae4..f69b87bc0 100644 --- a/doc/src/symex/sap/examples.md +++ b/doc/src/symex/sap/examples.md @@ -38,6 +38,7 @@ $ owi c ./poly.c -w1 --no-assert-failure-expression-printing owi: [ERROR] Assert failure model { symbol symbol_0 i32 4 + entry_point main } owi: [ERROR] Reached problem! [13] @@ -84,6 +85,7 @@ $ owi c ./poly2.c --no-assert-failure-expression-printing owi: [ERROR] Assert failure model { symbol symbol_0 i32 -2147483644 + entry_point main } owi: [ERROR] Reached problem! [13] @@ -135,6 +137,7 @@ $ owi c++ ./poly.cpp -w1 --no-assert-failure-expression-printing owi: [ERROR] Assert failure model { symbol symbol_0 i32 4 + entry_point main } owi: [ERROR] Reached problem! [13] @@ -181,6 +184,7 @@ $ owi c++ ./poly2.cpp --no-assert-failure-expression-printing owi: [ERROR] Assert failure model { symbol symbol_0 i32 -2147483644 + entry_point main } owi: [ERROR] Reached problem! [13] @@ -305,6 +309,7 @@ model { symbol symbol_25 i32 symbol symbol_26 i32 symbol symbol_27 i32 + entry_point main } owi: [ERROR] Reached problem! [13] @@ -371,6 +376,7 @@ model { symbol symbol_4 i32 symbol symbol_5 i32 symbol symbol_6 i32 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/doc/src/symex/verification/eacsl.md b/doc/src/symex/verification/eacsl.md index 187c31f9e..66c94f4d5 100644 --- a/doc/src/symex/verification/eacsl.md +++ b/doc/src/symex/verification/eacsl.md @@ -97,6 +97,7 @@ $ owi c --e-acsl primes.c -w1 owi: [ERROR] Assert failure: false model { symbol symbol_0 i32 2 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/src/bin/owi.ml b/src/bin/owi.ml index 93b55a142..c7f7a87de 100644 --- a/src/bin/owi.ml +++ b/src/bin/owi.ml @@ -150,10 +150,6 @@ let model_out_file = & opt (some path_conv) None & info [ "model-out-file" ] ~docv:"FILE" ~doc ) -let model_with_entry_point = - let doc = "Add the entry point in the generated model for easier replay." in - Arg.(value & flag & info [ "model-with-entry-point" ] ~doc) - let rac = let doc = "runtime assertion checking mode" in Arg.(value & flag & info [ "rac" ] ~doc) @@ -251,14 +247,12 @@ let c_cmd = and+ out_file and+ model_out_file and+ with_breadcrumbs - and+ model_with_entry_point and+ entry_point in Cmd_c.cmd ~arch ~property ~testcomp ~workspace ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~eacsl ~solver ~model_format ~entry_point ~invoke_with_symbols ~out_file ~model_out_file ~with_breadcrumbs - ~model_with_entry_point (* owi cpp *) let cpp_info = @@ -290,13 +284,12 @@ let cpp_cmd = and+ workspace and+ model_out_file and+ with_breadcrumbs - and+ model_with_entry_point and+ entry_point in Cmd_cpp.cmd ~arch ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format ~entry_point ~invoke_with_symbols ~out_file ~workspace ~model_out_file - ~with_breadcrumbs ~model_with_entry_point + ~with_breadcrumbs (* owi conc *) @@ -324,13 +317,11 @@ let conc_cmd = and+ model_out_file and+ invoke_with_symbols and+ with_breadcrumbs - and+ model_with_entry_point and+ entry_point in Cmd_conc.cmd ~unsafe ~rac ~srac ~optimize ~workers ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point ~invoke_with_symbols ~model_out_file ~with_breadcrumbs - ~model_with_entry_point (* owi fmt *) @@ -484,13 +475,12 @@ let rust_cmd = and+ workspace and+ model_out_file and+ with_breadcrumbs - and+ model_with_entry_point and+ entry_point in Cmd_rust.cmd ~arch ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format ~entry_point ~invoke_with_symbols ~out_file ~workspace ~model_out_file - ~with_breadcrumbs ~model_with_entry_point + ~with_breadcrumbs (* owi script *) @@ -535,13 +525,11 @@ let sym_cmd = and+ entry_point and+ model_out_file and+ with_breadcrumbs - and+ model_with_entry_point and+ invoke_with_symbols in Cmd_sym.cmd ~unsafe ~rac ~srac ~optimize ~workers ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point ~invoke_with_symbols ~model_out_file ~with_breadcrumbs - ~model_with_entry_point (* owi validate *) @@ -631,13 +619,11 @@ let zig_cmd = and+ model_out_file and+ () = setup_log and+ with_breadcrumbs - and+ model_with_entry_point and+ entry_point in Cmd_zig.cmd ~includes ~workers ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format ~entry_point ~invoke_with_symbols ~out_file ~workspace ~model_out_file ~with_breadcrumbs - ~model_with_entry_point (* owi *) diff --git a/src/cmd/cmd_c.ml b/src/cmd/cmd_c.ml index 1cca934bf..52d50ca8f 100644 --- a/src/cmd/cmd_c.ml +++ b/src/cmd/cmd_c.ml @@ -177,8 +177,8 @@ let cmd ~arch ~property ~testcomp:_ ~workspace ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~eacsl ~solver ~model_format ~(entry_point : string option) - ~invoke_with_symbols ~out_file ~model_out_file ~with_breadcrumbs - ~model_with_entry_point : unit Result.t = + ~invoke_with_symbols ~out_file ~model_out_file ~with_breadcrumbs : + unit Result.t = let* workspace = match workspace with | Some path -> Ok path @@ -201,4 +201,3 @@ let cmd ~arch ~property ~testcomp:_ ~workspace ~workers ~opt_lvl ~includes ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point ~invoke_with_symbols ~model_out_file ~with_breadcrumbs - ~model_with_entry_point diff --git a/src/cmd/cmd_c.mli b/src/cmd/cmd_c.mli index 2ca3fe926..a8416afcf 100644 --- a/src/cmd/cmd_c.mli +++ b/src/cmd/cmd_c.mli @@ -27,5 +27,4 @@ val cmd : -> out_file:Fpath.t option -> model_out_file:Fpath.t option -> with_breadcrumbs:bool - -> model_with_entry_point:bool -> unit Result.t diff --git a/src/cmd/cmd_conc.ml b/src/cmd/cmd_conc.ml index 4c4ba7cbc..b25dccc79 100644 --- a/src/cmd/cmd_conc.ml +++ b/src/cmd/cmd_conc.ml @@ -433,8 +433,7 @@ let assignments_to_model (assignments : (Smtml.Symbol.t * V.t) list) : let cmd ~unsafe ~rac ~srac ~optimize ~workers:_ ~no_stop_at_failure:_ ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order:_ ~fail_mode:_ ~workspace ~solver ~files ~model_format ~entry_point - ~invoke_with_symbols ~model_out_file ~with_breadcrumbs:_ - ~model_with_entry_point:_ = + ~invoke_with_symbols ~model_out_file ~with_breadcrumbs:_ = let* workspace = match workspace with | Some path -> Ok path diff --git a/src/cmd/cmd_conc.mli b/src/cmd/cmd_conc.mli index 3336824da..67cb88c98 100644 --- a/src/cmd/cmd_conc.mli +++ b/src/cmd/cmd_conc.mli @@ -21,5 +21,4 @@ val cmd : -> invoke_with_symbols:bool -> model_out_file:Fpath.t option -> with_breadcrumbs:bool - -> model_with_entry_point:bool -> unit Result.t diff --git a/src/cmd/cmd_cpp.ml b/src/cmd/cmd_cpp.ml index 0ddcd0016..367c83ea5 100644 --- a/src/cmd/cmd_cpp.ml +++ b/src/cmd/cmd_cpp.ml @@ -103,7 +103,7 @@ let cmd ~arch:_ ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format ~entry_point ~invoke_with_symbols ~out_file ~workspace ~model_out_file - ~with_breadcrumbs ~model_with_entry_point : unit Result.t = + ~with_breadcrumbs : unit Result.t = let* workspace = match workspace with | Some path -> Ok path @@ -124,4 +124,3 @@ let cmd ~arch:_ ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point ~invoke_with_symbols ~model_out_file ~with_breadcrumbs - ~model_with_entry_point diff --git a/src/cmd/cmd_cpp.mli b/src/cmd/cmd_cpp.mli index 8d9f6182a..9639480b5 100644 --- a/src/cmd/cmd_cpp.mli +++ b/src/cmd/cmd_cpp.mli @@ -24,5 +24,4 @@ val cmd : -> workspace:Fpath.t option -> model_out_file:Fpath.t option -> with_breadcrumbs:bool - -> model_with_entry_point:bool -> unit Result.t diff --git a/src/cmd/cmd_iso.ml b/src/cmd/cmd_iso.ml index 2ea3fe194..d4a092d06 100644 --- a/src/cmd/cmd_iso.ml +++ b/src/cmd/cmd_iso.ml @@ -443,6 +443,5 @@ let cmd ~deterministic_result_order ~fail_mode ~files ~model_format Cmd_sym.handle_result ~fail_mode ~workers ~solver ~deterministic_result_order ~model_format ~no_value ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure - ~model_out_file ~with_breadcrumbs ~model_with_entry_point:false - ~entry_point:None result ) + ~model_out_file ~with_breadcrumbs ~entry_point:None result ) () common_exports diff --git a/src/cmd/cmd_replay.ml b/src/cmd/cmd_replay.ml index e5b617f31..6936dc4e2 100644 --- a/src/cmd/cmd_replay.ml +++ b/src/cmd/cmd_replay.ml @@ -303,8 +303,11 @@ let cmd ~unsafe ~optimize ~replay_file ~source_file ~entry_point let entry_point = if Option.is_none entry_point then model_entry_point else entry_point in - Logs.debug (fun m -> m "%s" (Option.value ~default:"na" entry_point)); - Logs.debug (fun m -> m "%s" (Option.value ~default:"na" model_entry_point)); + Logs.debug (fun m -> + m "Specified entry point: %s" (Option.value ~default:"None" entry_point) ); + Logs.debug (fun m -> + m "Entry point inside model: %s" + (Option.value ~default:"None" model_entry_point) ); let+ () = run_file ~unsafe ~optimize ~entry_point ~invoke_with_symbols source_file model diff --git a/src/cmd/cmd_rust.ml b/src/cmd/cmd_rust.ml index c7e9a82b7..5752d9379 100644 --- a/src/cmd/cmd_rust.ml +++ b/src/cmd/cmd_rust.ml @@ -50,7 +50,7 @@ let cmd ~arch:_ ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format ~entry_point ~invoke_with_symbols ~out_file ~(workspace : Fpath.t option) - ~model_out_file ~with_breadcrumbs ~model_with_entry_point : unit Result.t = + ~model_out_file ~with_breadcrumbs : unit Result.t = let* workspace = match workspace with | Some path -> Ok path @@ -68,4 +68,3 @@ let cmd ~arch:_ ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point ~invoke_with_symbols ~model_out_file ~with_breadcrumbs - ~model_with_entry_point diff --git a/src/cmd/cmd_rust.mli b/src/cmd/cmd_rust.mli index 8d9f6182a..9639480b5 100644 --- a/src/cmd/cmd_rust.mli +++ b/src/cmd/cmd_rust.mli @@ -24,5 +24,4 @@ val cmd : -> workspace:Fpath.t option -> model_out_file:Fpath.t option -> with_breadcrumbs:bool - -> model_with_entry_point:bool -> unit Result.t diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml index fad5dee23..22d7e8453 100644 --- a/src/cmd/cmd_sym.ml +++ b/src/cmd/cmd_sym.ml @@ -34,8 +34,7 @@ let run_file ~entry_point ~unsafe ~rac ~srac ~optimize ~invoke_with_symbols _pc Interpret.Symbolic.modul link_state.envs m let print_bug ~model_format ~model_out_file ~id ~no_value ~no_stop_at_failure - ~no_assert_failure_expression_printing ~with_breadcrumbs - ~model_with_entry_point ~entry_point bug = + ~no_assert_failure_expression_printing ~with_breadcrumbs ~entry_point bug = let pp fmt (model, labels, breadcrumbs, scoped_values) = match model_format with | Cmd_utils.Json -> @@ -77,7 +76,8 @@ let print_bug ~model_format ~model_out_file ~id ~no_value ~no_stop_at_failure else model in let model = - if model_with_entry_point then + match entry_point with + | Some entry_point -> let ep = [ { Scfg.Types.name = "entry_point" ; params = [ entry_point ] @@ -86,7 +86,7 @@ let print_bug ~model_format ~model_out_file ~id ~no_value ~no_stop_at_failure ] in { model with children = model.children @ ep } - else model + | None -> model in Scfg.Pp.directive fmt model in @@ -131,7 +131,7 @@ let print_bug ~model_format ~model_out_file ~id ~no_value ~no_stop_at_failure let print_and_count_failures ~model_format ~model_out_file ~no_value ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure - ~count_acc ~results ~with_breadcrumbs ~model_with_entry_point ~entry_point = + ~count_acc ~results ~with_breadcrumbs ~entry_point = let test_suite_dir = Fpath.(workspace / "test-suite") in let* (_created : bool) = if not no_value then OS.Dir.create test_suite_dir else Ok false @@ -147,7 +147,7 @@ let print_and_count_failures ~model_format ~model_out_file ~no_value let* () = print_bug ~model_format ~model_out_file ~id:count_acc ~no_value ~no_stop_at_failure ~no_assert_failure_expression_printing - ~with_breadcrumbs ~model_with_entry_point ~entry_point bug + ~with_breadcrumbs ~entry_point bug in Ok model | `Error e -> Error e @@ -176,7 +176,7 @@ let sort_results deterministic_result_order results = let handle_result ~workers ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~workspace ~solver ~model_format ~model_out_file ~with_breadcrumbs - ~model_with_entry_point ~entry_point (result : unit Symbolic.Choice.t) = + ~entry_point (result : unit Symbolic.Choice.t) = let thread = Thread_with_memory.init () in let res_queue = Wq.make () in let path_count = Atomic.make 0 in @@ -207,16 +207,10 @@ let handle_result ~workers ~no_stop_at_failure ~no_value Array.iter Domain.join join_handles ) in let results = sort_results deterministic_result_order results in - let* entry_point = - if model_with_entry_point then - match entry_point with Some ep -> Ok ep | None -> Fmt.error_msg "" - else Ok "" - in let* count = print_and_count_failures ~model_format ~model_out_file ~no_value ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure - ~count_acc:0 ~results ~with_breadcrumbs ~model_with_entry_point - ~entry_point + ~count_acc:0 ~results ~with_breadcrumbs ~entry_point in Logs.info (fun m -> m "Completed paths: %d" (Atomic.get path_count)); let+ () = if count > 0 then Error (`Found_bug count) else Ok () in @@ -229,7 +223,7 @@ let handle_result ~workers ~no_stop_at_failure ~no_value let cmd ~unsafe ~rac ~srac ~optimize ~workers ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point ~invoke_with_symbols - ~model_out_file ~with_breadcrumbs ~model_with_entry_point = + ~model_out_file ~with_breadcrumbs = let* workspace = match workspace with | Some path -> Ok path @@ -246,5 +240,4 @@ let cmd ~unsafe ~rac ~srac ~optimize ~workers ~no_stop_at_failure ~no_value in handle_result ~fail_mode ~workers ~solver ~deterministic_result_order ~model_format ~no_value ~no_assert_failure_expression_printing ~workspace - ~no_stop_at_failure ~model_out_file ~with_breadcrumbs - ~model_with_entry_point ~entry_point result + ~no_stop_at_failure ~model_out_file ~with_breadcrumbs ~entry_point result diff --git a/src/cmd/cmd_sym.mli b/src/cmd/cmd_sym.mli index cb43e2351..835ddd7fe 100644 --- a/src/cmd/cmd_sym.mli +++ b/src/cmd/cmd_sym.mli @@ -23,7 +23,6 @@ val handle_result : -> model_format:Cmd_utils.model_format -> model_out_file:Fpath.t option -> with_breadcrumbs:bool - -> model_with_entry_point:bool -> entry_point:string option -> unit Symbolic.Choice.t -> unit Result.t @@ -47,5 +46,4 @@ val cmd : -> invoke_with_symbols:bool -> model_out_file:Fpath.t option -> with_breadcrumbs:bool - -> model_with_entry_point:bool -> unit Result.t diff --git a/src/cmd/cmd_zig.ml b/src/cmd/cmd_zig.ml index f6552e839..256b487c7 100644 --- a/src/cmd/cmd_zig.ml +++ b/src/cmd/cmd_zig.ml @@ -61,8 +61,7 @@ let compile ~workspace ~entry_point ~includes ~out_file (files : Fpath.t list) : let cmd ~workers ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format ~entry_point ~invoke_with_symbols - ~out_file ~workspace ~model_out_file ~with_breadcrumbs ~model_with_entry_point - : unit Result.t = + ~out_file ~workspace ~model_out_file ~with_breadcrumbs : unit Result.t = let* workspace = match workspace with | Some path -> Ok path @@ -86,4 +85,3 @@ let cmd ~workers ~includes ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point ~invoke_with_symbols ~model_out_file ~with_breadcrumbs - ~model_with_entry_point diff --git a/test/c/collections-c/tests_array.t b/test/c/collections-c/tests_array.t index 369ab2995..38a91c998 100644 --- a/test/c/collections-c/tests_array.t +++ b/test/c/collections-c/tests_array.t @@ -73,6 +73,7 @@ Array tests: symbol symbol_1 i32 0 symbol symbol_2 i32 0 symbol symbol_3 i32 0 + entry_point main } owi: [ERROR] Reached problem! diff --git a/test/c/collections-c/tests_buggy.t b/test/c/collections-c/tests_buggy.t index d227ab51e..acc8caa3f 100644 --- a/test/c/collections-c/tests_buggy.t +++ b/test/c/collections-c/tests_buggy.t @@ -4,6 +4,7 @@ Bug-triggering tests: owi: [ERROR] Trap: memory heap buffer overflow model { symbol symbol_0 i32 8 + entry_point main } owi: [ERROR] Reached problem! [13] @@ -22,6 +23,7 @@ Bug-triggering tests: symbol symbol_8 i32 symbol symbol_9 i32 symbol symbol_10 i32 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/test/c/collections-c/tests_pqueue.t b/test/c/collections-c/tests_pqueue.t index 3ba611242..ccfff8a77 100644 --- a/test/c/collections-c/tests_pqueue.t +++ b/test/c/collections-c/tests_pqueue.t @@ -10,6 +10,7 @@ Pqueue tests: symbol symbol_3 i32 symbol symbol_4 i32 symbol symbol_5 i32 + entry_point main } owi: [ERROR] Reached problem! @@ -29,6 +30,7 @@ Pqueue tests: symbol symbol_6 i32 symbol symbol_7 i32 symbol symbol_8 i32 + entry_point main } owi: [ERROR] Reached problem! diff --git a/test/c/double_free.t b/test/c/double_free.t index 0ec0dc759..00621fe7d 100644 --- a/test/c/double_free.t +++ b/test/c/double_free.t @@ -1,5 +1,7 @@ $ owi c double_free.c --entry-point=f owi: [ERROR] Trap: double free - model + model { + entry_point f + } owi: [ERROR] Reached problem! [13] diff --git a/test/c/eacsl/function/integer_dividable.t b/test/c/eacsl/function/integer_dividable.t index b27d2253b..bd9fb2451 100644 --- a/test/c/eacsl/function/integer_dividable.t +++ b/test/c/eacsl/function/integer_dividable.t @@ -3,6 +3,7 @@ model { symbol symbol_0 i32 symbol symbol_1 i32 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/test/c/eacsl/function/max.t b/test/c/eacsl/function/max.t index 8c04ea8c8..f53e8a05b 100644 --- a/test/c/eacsl/function/max.t +++ b/test/c/eacsl/function/max.t @@ -3,6 +3,7 @@ model { symbol symbol_0 i32 symbol symbol_1 i32 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/test/c/eacsl/function/max_ptr.t b/test/c/eacsl/function/max_ptr.t index ab1a66d01..1da990fec 100644 --- a/test/c/eacsl/function/max_ptr.t +++ b/test/c/eacsl/function/max_ptr.t @@ -3,6 +3,7 @@ model { symbol symbol_0 i32 symbol symbol_1 i32 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/test/c/eacsl/ghost/case.t b/test/c/eacsl/ghost/case.t index a9aff9ee7..f6db0bc19 100644 --- a/test/c/eacsl/ghost/case.t +++ b/test/c/eacsl/ghost/case.t @@ -2,6 +2,7 @@ owi: [ERROR] Assert failure: (bool.ne symbol_0 2) model { symbol symbol_0 i32 2 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/test/c/eacsl/ghost/default.t b/test/c/eacsl/ghost/default.t index 6764e6426..61bb8add4 100644 --- a/test/c/eacsl/ghost/default.t +++ b/test/c/eacsl/ghost/default.t @@ -2,6 +2,7 @@ owi: [ERROR] Assert failure: (i32.lt_u symbol_0 2) model { symbol symbol_0 i32 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/test/c/eacsl/ghost/else.t b/test/c/eacsl/ghost/else.t index abf66ad27..40f735a58 100644 --- a/test/c/eacsl/ghost/else.t +++ b/test/c/eacsl/ghost/else.t @@ -2,6 +2,7 @@ owi: [ERROR] Assert failure model { symbol symbol_0 i32 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/test/c/eacsl/ghost/global.t b/test/c/eacsl/ghost/global.t index 2d6d10115..445c7d485 100644 --- a/test/c/eacsl/ghost/global.t +++ b/test/c/eacsl/ghost/global.t @@ -2,6 +2,7 @@ owi: [ERROR] Assert failure: (i32.lt_s symbol_0 20) model { symbol symbol_0 i32 20 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/test/c/entry_point.t b/test/c/entry_point.t index e14805edf..f58c0b4c6 100644 --- a/test/c/entry_point.t +++ b/test/c/entry_point.t @@ -3,6 +3,7 @@ entry_point: owi: [ERROR] Assert failure: (i32.lt_s symbol_0 19) model { symbol symbol_0 i32 19 + entry_point fun } owi: [ERROR] Reached problem! [13] diff --git a/test/c/exit.t b/test/c/exit.t index 4a1870524..96dc358bd 100644 --- a/test/c/exit.t +++ b/test/c/exit.t @@ -2,6 +2,7 @@ owi: [ERROR] Assert failure: (i32.to_bool symbol_0) model { symbol symbol_0 i32 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/test/c/invisible_bool.t b/test/c/invisible_bool.t index 398a95d84..63298d086 100644 --- a/test/c/invisible_bool.t +++ b/test/c/invisible_bool.t @@ -2,6 +2,7 @@ owi: [ERROR] Assert failure: false model { symbol symbol_0 i1 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/test/c/invoke_with_symbols.t b/test/c/invoke_with_symbols.t index c31f44d7e..d06542a84 100644 --- a/test/c/invoke_with_symbols.t +++ b/test/c/invoke_with_symbols.t @@ -8,6 +8,7 @@ symbol symbol_1 i64 0 symbol symbol_2 f32 1. symbol symbol_3 f64 -1234. + entry_point f } owi: [ERROR] Reached problem! [13] diff --git a/test/c/label.t b/test/c/label.t index ee4cf0dc4..bc9bbbebc 100644 --- a/test/c/label.t +++ b/test/c/label.t @@ -3,11 +3,13 @@ model { symbol symbol_0 i32 50 label 1 label_1 + entry_point main } owi: [ERROR] Assert failure: false model { symbol symbol_0 i32 49 label 2 label_2 + entry_point main } owi: [ERROR] Reached 2 problems! [13] diff --git a/test/c/main.t b/test/c/main.t index 89f22a22b..b5b0328c6 100644 --- a/test/c/main.t +++ b/test/c/main.t @@ -7,6 +7,7 @@ symbol symbol_3 i8 symbol symbol_4 i8 symbol symbol_5 i8 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/test/c/malloc_zero.t b/test/c/malloc_zero.t index 2e543bf8b..ea4a59882 100644 --- a/test/c/malloc_zero.t +++ b/test/c/malloc_zero.t @@ -1,13 +1,17 @@ $ owi c ./malloc_zero.c --entry-point=f1 -w1 -O0 owi: [ERROR] Assert failure: false - model + model { + entry_point f1 + } owi: [ERROR] Reached problem! [13] $ owi c ./malloc_zero.c --entry-point=f2 -w1 -O0 All OK! $ owi c ./malloc_zero.c --entry-point=g1 -w1 -O0 owi: [ERROR] Assert failure: false - model + model { + entry_point g1 + } owi: [ERROR] Reached problem! [13] $ owi c ./malloc_zero.c --entry-point=g2 -w1 -O0 diff --git a/test/c/model_with_entry_point.t b/test/c/model_with_entry_point.t index d3760a555..75bcd3c8d 100644 --- a/test/c/model_with_entry_point.t +++ b/test/c/model_with_entry_point.t @@ -1,4 +1,4 @@ - $ owi c model_with_entry_point.c --model-with-entry-point -O0 --entry-point=main + $ owi c model_with_entry_point.c -O0 --entry-point=main owi: [ERROR] Assert failure: (bool.eq symbol_0 3) model { symbol symbol_0 i32 2 @@ -7,7 +7,7 @@ owi: [ERROR] Reached problem! [13] - $ owi c model_with_entry_point.c --model-with-entry-point -O0 --entry-point=fun + $ owi c model_with_entry_point.c -O0 --entry-point=fun owi: [ERROR] Assert failure: (bool.eq symbol_0 2) model { symbol symbol_0 i32 1 @@ -16,7 +16,7 @@ owi: [ERROR] Reached problem! [13] - $ owi c model_with_entry_point.c --model-with-entry-point -O0 --entry-point=fun --model-out-file=output.scfg -o output.wasm + $ owi c model_with_entry_point.c -O0 --entry-point=fun --model-out-file=output.scfg -o output.wasm owi: [ERROR] Assert failure: (bool.eq symbol_0 2) owi: [ERROR] Reached problem! [13] diff --git a/test/c/range.t b/test/c/range.t index 34738fb03..3a21e12fd 100644 --- a/test/c/range.t +++ b/test/c/range.t @@ -3,6 +3,7 @@ model { symbol symbol_0 i32 16 symbol symbol_1 i32 100 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/test/c/scopes.t b/test/c/scopes.t index 7eba0d25d..5b118df7f 100644 --- a/test/c/scopes.t +++ b/test/c/scopes.t @@ -17,6 +17,7 @@ } symbol symbol_8 i32 aaa symbol symbol_9 i32 aaa + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/test/c/test-comp/simple.t b/test/c/test-comp/simple.t index a92d6d6a4..e033669e8 100644 --- a/test/c/test-comp/simple.t +++ b/test/c/test-comp/simple.t @@ -2,6 +2,7 @@ owi: [ERROR] Assert failure: (bool.ne (i32.mul symbol_0 symbol_0) 0) model { symbol symbol_0 i32 0 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/test/cpp/entry_point.t b/test/cpp/entry_point.t index c5faf1a9d..f46f6a490 100644 --- a/test/cpp/entry_point.t +++ b/test/cpp/entry_point.t @@ -3,6 +3,7 @@ entry_point: owi: [ERROR] Assert failure: (i32.lt_s symbol_0 19) model { symbol symbol_0 i32 19 + entry_point fun } owi: [ERROR] Reached problem! [13] diff --git a/test/replay/alloc.t b/test/replay/alloc.t index 0b19e39b2..69eba480a 100644 --- a/test/replay/alloc.t +++ b/test/replay/alloc.t @@ -2,6 +2,7 @@ owi: [ERROR] Assert failure: false model { symbol symbol_0 i32 + entry_point main } owi: [ERROR] Reached problem! [13] diff --git a/test/rust/entry_point.t b/test/rust/entry_point.t index 3943f0a98..9d65c48ec 100644 --- a/test/rust/entry_point.t +++ b/test/rust/entry_point.t @@ -3,6 +3,7 @@ entry_point: owi: [ERROR] Assert failure: (i32.le_s 4 symbol_0) model { symbol symbol_0 i32 2 + entry_point fun } owi: [ERROR] Reached problem! [13] diff --git a/test/sym/entry_points/export.t b/test/sym/entry_points/export.t index 2b5c6259c..848f23c17 100644 --- a/test/sym/entry_points/export.t +++ b/test/sym/entry_points/export.t @@ -10,6 +10,7 @@ export: owi: [ERROR] Assert failure: (i32.lt_u symbol_0 19) model { symbol symbol_0 i32 19 + entry_point fun } owi: [ERROR] Reached problem! [13] diff --git a/test/sym/print_pc.t b/test/sym/print_pc.t index 0648d26bc..767ffb057 100644 --- a/test/sym/print_pc.t +++ b/test/sym/print_pc.t @@ -115,5 +115,6 @@ owi: [DEBUG] Current scope tokens: [symbol symbol_0] model { symbol symbol_0 i32 0 + entry_point f } owi: [ERROR] Reached problem! diff --git a/test/zig/entry_point.t b/test/zig/entry_point.t index ca4a58a91..13bd51960 100644 --- a/test/zig/entry_point.t +++ b/test/zig/entry_point.t @@ -3,6 +3,7 @@ entry_point: owi: [ERROR] Assert failure: (i32.le_s 5 symbol_0) model { symbol symbol_0 i32 4 + entry_point fun } owi: [ERROR] Reached problem! [13]