eth-sri / ELINA

ELINA: ETH LIbrary for Numerical Analysis
http://elina.ethz.ch/
Other
129 stars 54 forks source link

Segmentation fault in substitution #97

Open McTsts opened 3 months ago

McTsts commented 3 months ago

Hello, I'm trying to use substitution with the apron interface and am encountering segmentation faults whenever one of Abstract1's texpr substitution functions are called.

Here's a simple example that causes a segmentation fault for me:

open Apron

let () =
  (* manager *)
  let manager = Elina_oct.manager_alloc () in

  (* Setup the Environment*)
  let vars = [| Var.of_string "x"; Var.of_string "y" |] in
  let env = Environment.make [||] vars in

  (* Create AbsVal *)
  let abs_val = Abstract1.top manager env in

  (* Create X, Y and Substitution *)
  let y = Texpr1.Var (Var.of_string "y") in
  let x = Var.of_string "x" in
  let substitution = Texpr1.of_expr env y in

  (* Substitute *)
  Abstract1.substitute_texpr_with manager abs_val x substitution None

The same also happens with Elina_poly manager. I've also tried the substitute_texpr function, but I'm encountering the same issue there. With the apron managers no issue occurs.