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庫引發了分段錯誤

回答

相關問題