PPL-devel

Download

ppl-devel@bugseng.com

October 2025

1 discussions

Re: Disjunction of two Pointset_Powerset? (likely bug in the OCaml binding)
by BUGSENG Support 04 Nov '25

04 Nov '25

Dear Étienne, thank you for contacting us directly. The ppl-devel mailing list has been relocated under a different domain (bugseng.com) we did not receive you emails. A notice informing of the relocation has been sent to all mailing list subscribers on Jan 22. Subject was: "PPL-devel mailing list relocation". Please, see the new PPL-devel home at: https://support.bugseng.com/cgi-bin/mailman/listinfo/ppl-devel Thank you for the bug report, we will look at it as soon as possible. Can you please share with us a testcase to reproduce the error? Do you have any additional information that might be helpful? Thank you, regards Federico On 08/11/24 14:00, Étienne André wrote: > Dear PPL developers, > > I received a "mailer daemon" in reply to my former email related to a > likely bug in the OCaml interface, so I take the liberty to write > another email (see below). > > Many thanks for your answer. > > Best, > > Étienne André > Université Sorbonne Paris Nord > https://lipn.univ-paris13.fr/~andre/ > > Le 22/10/2024 à 15:09, Étienne André a écrit : >> >> Dear PPL developers, >> >> We didn't have news since March, but we tried to investigate the >> problem, and it looks now rather likely to us that the bug mentioned >> in my first email /does/ come from a bug in PPL, more precisely from >> the OCaml binding. It is likely that some "free" operations on >> pointers in the binding are unnecessary, and cause the garbage >> collector to access some already destroyed objects, leading to >> segmentation faults. >> >> My colleagues are trying to fix the binding so as to remove the "free" >> operations, and let the OCaml garbage collector do its job naturally. >> >> We still want to point out this issue, and we do encourage you in >> investigating this matter. >> >> Best, >> >> Étienne André >> Université Sorbonne Paris Nord >> https://lipn.univ-paris13.fr/~andre/ >> >>> Em sex., 31 de mai. de 2024 às 13:34, Étienne André >>> <Andre.Etienne(a)lipn13.fr> escreveu: >>> >>> Dear PPL developers, >>> >>> I wonder whether you had received our email, and might have an >>> idea of why we encounter an issue of corrupted memory with >>> Pointset_Powerset. >>> >>> Thank you! >>> >>> Best, >>> >>> Étienne André >>> Université Sorbonne Paris Nord >>> https://lipn.univ-paris13.fr/~andre/ >>> >>> Le 18/03/2024 à 11:09, Étienne André a écrit : >>>> >>>> Dear PPL developers, >>>> >>>> We got an issue in developing IMITATOR with the PPL OCaml >>>> binding, most probably not related to a PPL bug (even if we >>>> don't fully exclude it either). >>>> >>>> Our goal is to perform the disjunction of two Pointset_Powerset, >>>> i.e., union_assign p1 p2, where p1 gets as the result the union >>>> of p1 and p2. >>>> >>>> I don't think there is a function to directly do this in PPL? If >>>> there is, which one should we use? >>>> >>>> Our algorithm is as follows: >>>> >>>> 1. get all disjuncts of p2 (using an iterator) >>>> 2. for each disjunct, add it to p1 using the PPL OCaml binding >>>> function ppl_Pointset_Powerset_NNC_Polyhedron_add_disjunct >>>> >>>> Is that the right way to do? >>>> >>>> >>>> We got dimensions exceptions, both very random (changing the >>>> input file name yields a different exception!) and with >>>> completely funny dimensions (such as 208 or 416) for a system >>>> that has only 2 dimensions, and/or segmentation faults/core dump >>>> which might come from a corrupted memory somewhere. >>>> >>>> We use OCaml 4.14.1 with (presumably) PPL 1:1.2-8.1build1. >>>> >>>> Thanks! >>>> >>>> Best, >>>> >>>> -- >>>> Étienne André >>>> Université Sorbonne Paris Nord >>>> https://lipn.univ-paris13.fr/~andre/ >>> >>> >>> >>> -- >>> att. Tomaz Gomes

2 2