Skip to content
  • Alexandre Duret-Lutz's avatar
    [buddy] fix undefined behavior · 787e3f93
    Alexandre Duret-Lutz authored
    The bug was found while running Spot's src/tgbatest/randpsl.test
    on Debian i386 with gcc-4.9.2.  The following call would crash:
    
    ./ltl2tgba -R3 -t '(!(F(({{{(p0) |
    {[*0]}}:{{{(p1)}[*2]}[:*]}[*]:[*2]}[:*0..3]}[]-> (G(F(p1)))) &
    (G((!(p1)) | ((!(p2)) W (G(!(p0)))))))))'
    
    On amd64 the call does not crash, but valgrind nonetheless
    report that uninitialized memory is being read by bdd_gbc()
    during the second garbage collect.
    
    * src/kernel.h (PUSHREF): Define as a function rather than a macro
    to avoid undefined behavior.  See comments for details.
    787e3f93