1. 30 Mar, 2017 1 commit
  2. 14 Mar, 2017 1 commit
  3. 13 Mar, 2017 1 commit
  4. 01 Feb, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      [buddy] fix some -Wpedantic messages · a2f174f7
      Alexandre Duret-Lutz authored
      * src/bddop.c: Empty macro arguments are undefined ISO C90 and
      ISO C++98.  Use '+' when calling APPLY_SHORTCUTS.
      * src/fdd.c, src/kernel.c: Avoid constructs invalid in C90.
      * src/bddop.c, src/bddx.h, src/kernel.c, src/kernel.h,
      examples/cmilner/cmilner.c: Remove C++ comments.
  5. 14 Jan, 2017 1 commit
  6. 19 Nov, 2016 1 commit
  7. 09 Nov, 2016 2 commits
  8. 08 Nov, 2016 1 commit
  9. 28 Oct, 2016 1 commit
  10. 20 Oct, 2016 2 commits
  11. 19 Oct, 2016 1 commit
  12. 27 Jul, 2016 1 commit
  13. 10 Nov, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      Use -Bsymbolic-functions and -Bsymbolic · 86abd6c1
      Alexandre Duret-Lutz authored
      This avoids dynamic lookups to resolve symbols inside the library, but
      disallows symbol interposition.
      * m4/symbolic.m4: New file.
      * buddy/m4/symbolic.m4: New link.
      * configure.ac, buddy/configure.ac: Add AX_SYMBOLIC.
      * buddy/src/Makefile.am, iface/ltsmin/Makefile.am, src/Makefile.am,
      wrap/python/Makefile.am: Link with $(SYMBOLIC_LDFLAGS).
  14. 24 Apr, 2015 1 commit
    • Etienne Renault's avatar
      Remove all cvsignore files. · 5f4b7e1f
      Etienne Renault authored
      * .cvsignore, bench/.cvsignore,
      bench/emptchk/.cvsignore, bench/emptchk/models/.cvsignore,
      bench/ltl2tgba/.cvsignore, buddy/.cvsignore,
      buddy/doc/.cvsignore, buddy/examples/.cvsignore,
      buddy/src/.cvsignore, buddy/tools/.cvsignore,
      doc/.cvsignore, iface/.cvsignore,
      src/.cvsignore, src/ltlast/.cvsignore,
      src/ltlenv/.cvsignore, src/ltlparse/.cvsignore,
      src/ltlvisit/.cvsignore, src/misc/.cvsignore,
      src/sanity/.cvsignore, src/tests/.cvsignore,
      src/twa/.cvsignore, tools/.cvsignore,
      wrap/.cvsignore, wrap/python/.cvsignore,
      wrap/python/tests/.cvsignore: here.
  15. 11 Mar, 2015 1 commit
  16. 10 Mar, 2015 1 commit
    • 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.
  17. 19 Nov, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      hoa: preliminary implementation of a parser · e55bcd95
      Alexandre Duret-Lutz authored
      * src/hoaparse/Makefile.am, src/hoaparse/fmterror.cc,
      src/hoaparse/hoaparse.yy, src/hoaparse/hoascan.ll,
      src/hoaparse/parsedecl.hh, src/hoaparse/public.hh: New files.
      * src/Makefile.am, configure.ac, README: Adjust.
      * src/tgbatest/ltl2tgba.cc: Add a -XH option.
      * src/tgbatest/hoaparse.test: New file.
      * src/tgbatest/Makefile.am: Adjust.
      * buddy/src/bddx.h: Add a bdd_from_int() function.
  18. 30 Oct, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      buddy: rename libbdd to libbddx · ad8d2422
      Alexandre Duret-Lutz authored
      * buddy/src/bdd.h, buddy/src/bvec.h, buddy/src/fdd.h: Rename as...
      * buddy/src/bddx.h, buddy/src/bvecx.h, buddy/src/fddx.h: ... these.
      * buddy/src/Makefile.am: Build libbddx.la instead of libbdd.la.
      * buddy/examples/Makefile.def: Use it.
      * Makefile.am, buddy/src/bddtest.cxx, buddy/src/bvec.c,
      buddy/src/cppext.cxx, buddy/src/fdd.c, buddy/src/imatrix.h,
      buddy/src/kernel.h, buddy/examples/adder/adder.cxx,
      buddy/examples/bddcalc/parser_.h, buddy/examples/bddtest/bddtest.cxx,
      buddy/examples/cmilner/cmilner.c, buddy/examples/fdd/fdd.cxx,
      buddy/examples/milner/milner.cxx, buddy/examples/money/money.cxx,
      buddy/examples/queen/queen.cxx, buddy/examples/solitare/solitare.cxx,
      m4/buddy.m4, src/ltlvisit/apcollect.hh, src/ltlvisit/simplify.hh,
      src/misc/bddlt.hh, src/misc/bddop.hh, src/misc/minato.hh,
      src/priv/acccompl.hh, src/priv/accconv.hh, src/priv/accmap.hh,
      src/priv/bddalloc.cc, src/tgba/bdddict.hh, src/tgba/bddprint.hh,
      src/tgba/tgbamask.hh, src/tgba/tgbasafracomplement.cc,
      src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/sccstack.hh,
      src/tgbaalgos/neverclaim.cc, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccinfo.hh,
      src/tgbaalgos/weight.hh, wrap/python/buddy.i: Adjust.
      * NEWS, README: Document it.
  19. 28 Oct, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      [buddy] pack cache entry on 16 bytes, not 20. · 971788fd
      Alexandre Duret-Lutz authored
      The double result is never used with a triple keys,
      so we can pack the cache entry more tightly.
      * src/cache.h: Reorganize the cache entry the structure.
      * src/cache.c: Cleanup the code while we are at it.
      * src/bddop.c: Adjust to accesses to cache entries.
  20. 11 Aug, 2014 2 commits
    • Alexandre Duret-Lutz's avatar
      [buddy] Fix a harmless uninitialized read. · d4e3a952
      Alexandre Duret-Lutz authored
      This can only cause failure when running under valgrind (i.e., in the
      test suite), but is not a problem in practice as the test is certain
      to fail the entry->c check whenever entry->b is uninitialized.
      * src/bddop.c (bdd_implies): Here.
    • Alexandre Duret-Lutz's avatar
      [buddy] Fix a harmless uninitialized read. · 1244b617
      Alexandre Duret-Lutz authored
      This can only cause failure when running under valgrind (i.e., in the
      test suite), but is not a problem in practice as the test is certain
      to fail the entry->c check whenever entry->b is uninitialized.
      * src/bddop.c (bdd_implies): Here.
  21. 20 Jun, 2014 1 commit
  22. 12 Feb, 2014 1 commit
  23. 29 Jul, 2013 2 commits
    • Alexandre Duret-Lutz's avatar
      [buddy] Probe for -fvisibility and -fvisibility-inlines-hidden. · cee55268
      Alexandre Duret-Lutz authored
      * configure.ac: Check gcc and g++ for -fvisibility and
      -fvisibility-inlines-hidden.  Add these options to
      * m4/ax_check_compile_flag.m4: New file.
      * src/Makefile.am: Build BuDDy as a single library, reverting part of
      the changes introduced in my previous patch to this file.  Since
      the options are set in CFLAGS/CXXFLAGS, there is no possibility
      for -fvisibility-inlines-hidden to be passed to the C compiler.
    • Alexandre Duret-Lutz's avatar
      [buddy] Restrict the number of exported symbols. · b5710663
      Alexandre Duret-Lutz authored
      * src/bdd.h, src/bvec.h, src/fdd.h: Declare all exported
      symbols using BUDDY_API, a new macro that sets visibility=default.
      * src/Makefile.am: Compile with -fvisibility=hidden by default,
      and compile the C++ part with -fvisibility-inlines-hidden as well.
  24. 24 Dec, 2012 1 commit
  25. 22 Aug, 2012 1 commit
  26. 19 Jun, 2012 2 commits
    • Alexandre Duret-Lutz's avatar
      [buddy] Add a function bdd_implies to decide implications between BDDs. · a814b975
      Alexandre Duret-Lutz authored
      * src/bdd.h (bdd_implies): New function.
      * src/bddop.c (bdd_implies): Implement it.
      (CACHEID_IMPLIES, IMPLIES_HASH): New helper macros.
    • Alexandre Duret-Lutz's avatar
      [buddy] Reduce the size of bddNode to improve cache efficiency. · e7a46e10
      Alexandre Duret-Lutz authored
      The unicity table was mixed with the bddNode table for now
      apparent reason.  After the hash of some node is computed,
      bddnodes[hash] did only contain some random node (not the one
      looked for) whose .hash member would point to the actual node with
      this hash.  So that's a two step lookup.  With this patch, we sill
      have a two step lookup, but the .hash member have been moved to a
      separate array.  A consequence is that bddNode is now 16-byte long
      (instead of 20) so it will never span across two cache lines.
      * src/kernel.h (bddNode): Remove the hash member, and move it...
      (bddhash): ... as this new separate table.
      * src/kernel.c, src/reorder.c: Adjust all code.
  27. 28 Apr, 2012 1 commit
  28. 28 Aug, 2011 1 commit
  29. 14 Jun, 2011 1 commit
  30. 09 Jun, 2011 1 commit
  31. 30 Apr, 2011 3 commits
  32. 10 Apr, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      [buddy] · e5f35dea
      Alexandre Duret-Lutz authored
      Fix some warnings reported by gcc.
      * buddy/src/kernel.c (errorstrings): Mark these as const.
      * buddy/src/reorder.c (reorder_gbc): Fix prototype.
      (siftTestCmp): Add missing const in cast.
      (bdd_reorder_auto): Actually call bdd_reorder_ready().
  33. 05 Apr, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      [buddy] · 5fdfe286
      Alexandre Duret-Lutz authored
      Tag functions with attributes pure, const, or noreturn.
      * src/bdd.h (__purefn, __constfn, __noreturnfn): Define
      new macros.
      * src/bdd.h, src/bddio.c, src/bvec.h, src/imatrix.h: Use them
      to tag many functions as suggested by -Wsuggest-attribute=pure,
      -Wsuggest-attribute=const, -Wsuggest-attribute=noreturn.