If you have encountered a problem with DIVINE, please check below whether there is an active ticket for your issue. Otherwise, please login with GitHub and report your issue. Thank you.

{5} Accepted, Active Tickets by Owner (Full Description) (8 matches)

List tickets accepted, group by ticket owner. This report demonstrates the use of full-row display.

mornfall (5 matches)

Ticket Summary Component Milestone Type Created
Description
#43 Fix thread_local VM 4.5 defect 01/21/2019

Currently, the thread_local keyword is not supported. Even worse, it is silently ignored: 

#include <thread>
#include <cassert>

thread_local int v;

int main()
{
    v = 42;
    std::thread t( [] {
        assert( v == 0 );
        v = 16;
        assert( v == 16 );
    } );
    assert( v == 42 );
    t.join();
}
#87 Struct self-assignment results in assertion failure in memcpy DiOS 4.3 defect 10/08/2019

Hi, the following code makes Divine 4.3.6 crash with an assertion failure in the DiOS's implementation of memcpy. While it is true, that the memory passed to memcpy should not overlap, the struct self-assignment should be permitted.

Thanks. 

int main(void)
{
    struct {
        char a;
        int  i;
    } s;
    s = s;
}
#95 sim: Integers < -5 appearing in dbg.value are discarded. sim 4.4 defect 10/21/2019

Hello, if I run the following code in the divine sim (occurs also on next builds): 

  int main(void)
  {
      int a = -1;
      int b = -5;
      return 0;
  }

the show command outputs: 

   > show
   attributes:
       address: heap* 1f78a5dd 0+0
       size:    16
       pc:      code* 80001 0
       location: test3.c:5
       symbol:  main
   .a:
       type:    int
       value:   [i32 4294967295 d]
       scope:   main
   related:     [ caller ]
   # executing main at test3.c:5

where the b variable entry is missing. Thanks!

#105 make: Move any compilation out of make install other 4.4 feature 01/21/2020

Hi, would it be possible to build everything even before the make install target is executed? At the moment, the nightly builds do not execute this target, and therefore, some compilation errors (e.g. shoop in 4.4.1) are left unnoticed. Thanks.

#44 Multi-Threaded Performance Doesn't Scale other 5.0 defect 01/25/2019

On my Debian laptop, I noticed that running divine check on my model took 30s for one thread, 23s for two threads, and 21s for four threads. The serial part in the beginning took around 10 seconds. I'm currently running divine check on a bigger model on a virtual machine (Also running Debian 9) with 32 CPUs and the performance, in terms of Mips and states per second, doesn't seem to be basically any better than with a single thread. It looks like all the CPU cores do produce heat, but they're spending most of the time in kernel space. Could there be a race for locks going on between the model checking threads or something?

My models are part of the ADAPRO project in GitLab?: ​https://gitlab.com/jllang/adapro I wrote this nice BASH script for running DIVINE on them. It requires some extra utilities, like bc, pgrep, and gnuplot, though.

Vladimír Štill (3 matches)

Ticket Summary Component Milestone Type Created
Description
#94 sim: Signed integer value is shown as unsigned. sim 4.4 defect 10/21/2019

Hello, if I run the following code in the divine sim (occurs also on next builds): 

  int main(void)
  {
      int a = -1;
      return 0;
  }

the show .x command outputs: 

  # executing main at test4.c:4
  > show
  attributes:
      address: heap* 1f78a5dd 0+0
      size:    16
      pc:      code* 80001 0
      location: test4.c:4
      symbol:  main
  .a:
      type:    int
      value:   [i32 4294967295 d]
      scope:   main
  related:     [ caller ]

where the a value should be interpreted as signed, i.e. -1, instead. Thanks!

#106 make: CMake does not set PYTHON_INTERP during libcxx configuration other 4.4 defect 01/28/2020

Hi, as previously discussed in the comments 6-10 of issue #73, the make install target still fails to complete without some additional downstream patching. This issue occurs on Fedora, Manjaro, Ubuntu (and probably on other Linux distros too). Thanks.

#92 divine info is outdated DiOS 4.3 defect 10/17/2019

Hello, the divine info command prints outdated DiOS options. For example, the listed -o ignore:arithmetic option is no longer valid (and subsequently ends with an out of bounds memory access warning), and on the other hand the -o ignore:exit option is not listed at all. Thanks!

Note: See TracReports for help on using and creating reports.