Z3的OCaml库引发了分段错误

考虑使用Z3模块与Z3解算器接口的以下OCaml代码片段。代码试图定义Z3新TPair数据类型与接受两个整数参数一个构造函数T：Z3的OCaml库引发了分段错误

open Z3                       
open Z3.SMT 
open Z3.Expr                      
open Z3.Symbol                     
open Z3.Datatype                     
open Z3.FuncDecl 
open Z3.Arithmetic 
open Z3.Arithmetic.Integer                  
open Z3.Quantifier 

let _ =                       
    let cfg = [("model", "true"); ("proof", "false")] in 
    let ctx = (mk_context cfg) in 
    let sym = Symbol.mk_string ctx in 
    let s_Int = mk_sort ctx in 
    (* (declare-datatypes() ((TPair (T Int Int))))*) 
    let s_T = mk_constructor_s ctx "T" (sym "isT") 
       [sym "left"; sym "right"]               
       [Some s_Int; Some s_Int] [0; 0] in            
    let s_TPair = mk_sort_s ctx "TPair" [s_T] in 
    let _::s_content::_ = Constructor.get_accessor_decls s_T in         
    let s_isT = Constructor.get_tester_decl s_T in             
    let solver = Solver.mk_solver ctx None in 
    begin 
     Printf.printf "***** CONTEXT ******\n";             
     print_string @@ Solver.to_string solver; 
     Printf.printf "\n*********************\n" 
    end

到get_tester_decl和get_accessor_decls都扔分割故障的电话。可能是什么原因？

来源

2016-10-06 Gowtham Kaki

报告给图书馆的作者。 – camlspotter

这里给出的示例源代码编译（带有警告）并且对我运行良好。 OCaml有一点点缺陷。您能否告诉我们您正在使用哪个版本以及从哪里获得？此外，请确保您使用的是最新的Z3源代码，并从源代码编译，因为自上次二进制发行版以来，已有多个修复程序。 –

没有用纯OCaml编写的代码会导致分段错误。这是因为OCaml是一种内存安全的语言。问题出在管道的某处，无论是在OCaml绑定到底层库的地方，还是在z3库本身。

只有库（或绑定）作者可以帮助您调试和解决此问题。所以请在the upstream存储库中创建一个问题。

来源

2016-10-07 13:07:31 ivg

感谢您的回答。这个问题是针对Z3社区的，因此我删除了OCaml标签。任何原因你重新添加它？ –

当然，这个问题在标题和正文中明确指出了OCaml，它还包含了OCaml代码。它看起来像OP认为，在OCaml或他的代码中的问题，而不是在图书馆。所以，我的任务是解释，OCaml本身不能成为这类问题的理由，所以应该在别处寻找问题的根源。我希望，在未来，我的回答会帮助那些会明确表示问题不在OCaml代码中的人来搜索“分段错误+ ocaml”。 – ivg

Z3的OCaml库引发了分段错误

回答

相关问题