Commits · e54ccb17255ed61cecf7309ee7f9f020e09abbfb · paradise / mirror / DIVINE · GitLab

Oct 19, 2019
- MC: Rewrite the code for weaver-based counterexample generation. · e54ccb17
  Petr Rockai authored Oct 19, 2019
  
  e54ccb17
- MC: Make the 'start' task a broadcast by default. · 56a95432
  Petr Rockai authored Oct 19, 2019
  
  56a95432
- MC: Prevent the weaver from delivering messages back to their origin machines. · faae79e1
  Petr Rockai authored Oct 19, 2019
  
  faae79e1
- MC: Indicate errors discovered in the program via weaver events. · 75e43bfc
  Petr Rockai authored Oct 19, 2019
  
  75e43bfc
- MC: Add a dedup_state task type (to be used in counterexample generation). · 5b5d7a68
  Petr Rockai authored Oct 19, 2019
  
  5b5d7a68
- MC: Allow replies to optionally set a new message identifier. · 9a6d483c
  Petr Rockai authored Oct 19, 2019
  
  9a6d483c
- MC: Implement a multi-type (variant-like) queue for the task weaver. · 12f15790
  Petr Rockai authored Oct 19, 2019
  
  12f15790
- bricks: Fix handling of references passed into the cons_list_t type alias. · 13bbebbc
  Petr Rockai authored Oct 19, 2019
  
  13bbebbc
- bricks: Allow types to be extracted from cons lists using indices. · 5dec467d
  Petr Rockai authored Oct 19, 2019
  
  5dec467d
- bricks: Add a static constexpr 'size' member to cons lists. · 71ee4bfd
  Petr Rockai authored Oct 19, 2019
  
  71ee4bfd
- bricks: Allow value-based (as opposed to reference-based) views of cons lists. · f2046ce7
  Petr Rockai authored Oct 19, 2019
  
  f2046ce7
Oct 18, 2019
- MC: Update machine unit tests. · fe526453
  Petr Rockai authored Oct 18, 2019
  
  fe526453
- MC: Actually use a solver for exec --symbolic. · 34904814
  Petr Rockai authored Oct 18, 2019
  
  34904814
- VM: Add a few missing const qualifiers to context methods. · 8fb746f3
  Petr Rockai authored Oct 18, 2019
  
  8fb746f3
- MC: Fix detection of infeasible paths in exec. · cf365704
  Petr Rockai authored Oct 18, 2019
  
  cf365704
- MC: Adapt the backtrack mechanism in exec to the new machine design. · e6baeee8
  Petr Rockai authored Oct 18, 2019
  
  e6baeee8
- MC: Disentangle the complex machine stack into a pair of simpler classes. · 110e11d7
  Petr Rockai authored Oct 18, 2019
  
  110e11d7
- MC: Allow Hasher to be attached to a heap post-construction. · 71a6ec7c
  Petr Rockai authored Oct 18, 2019
  
  71a6ec7c
- MC: Add a reply() method to machine_base. · e907cbfe
  Petr Rockai authored Oct 18, 2019
  
  e907cbfe
Oct 16, 2019
- MC: Allow more control over weaver task assignment. · adac4fbb
  Petr Rockai authored Oct 16, 2019
  
  adac4fbb
- MC: Do not retrace already resolved subpaths when generating counterexamples. · 012a5bd2
  Petr Rockai authored Oct 16, 2019
  
  012a5bd2
- MC: Keep track of the choices made when tracing counterexamples. · af5ea135
  Petr Rockai authored Oct 16, 2019
  
  af5ea135
- MC: First draft of weaver-based counterexample generation. · 1979d3fb
  Petr Rockai authored Oct 15, 2019
  
  1979d3fb
Oct 18, 2019
- test: Update the list of brick unit tests. · 15bdb704
  Petr Rockai authored Oct 18, 2019
  
  15bdb704
- dios: Fix a memory leak in fs::VmBuffTraceFile. · c72d9ab7
  Petr Rockai authored Oct 18, 2019
  
  c72d9ab7
- VM: Do not leak debug-persisted objects when they are freed by the program. · 5db446b1
  Petr Rockai authored Oct 18, 2019
  
  5db446b1
Oct 16, 2019
- test: Remove obsolete libc++ tests as they were replaced by newer versions. · fa494bf0
  Lukáš Korenčik authored Oct 16, 2019
  
  fa494bf0
- test: Port libc++ v9.0 tests for containers. · 4477abeb
  Lukáš Korenčik authored Oct 16, 2019
  
  4477abeb
- test: Add missing ext and big tags. · d0aaaf90
  Lukáš Korenčik authored Oct 16, 2019
  
  d0aaaf90
Oct 17, 2019
- bricks: Rename the brq_t namespace to t_brq (so it doesn't look like a type). · eea470e0
  Petr Rockai authored Oct 17, 2019
  
  eea470e0
- cmake: Install some additional tools (divcc, dioscc, lart). · ea2ef344
  Petr Rockai authored Oct 17, 2019
  
  ea2ef344
- bricks: Fix constexpr violations in shift operators in bitlevel::bvpair. · 65b19cc2
  Petr Rockai authored Oct 17, 2019
  
  65b19cc2
- bricks: Fix catch clauses in brick-unittest. · 4f7e9a4b
  Petr Rockai authored Oct 17, 2019
  
  4f7e9a4b
- cmake: Make sure that common options are also applied to libdivine-sim. · 54254a59
  Petr Rockai authored Oct 17, 2019
  
  54254a59
Oct 16, 2019
- bricks: Add the equality operator to RPN::Variable. · 17647346
  Zuzana Baranová authored Oct 16, 2019
  
  17647346
Oct 15, 2019
- smt: Insert a 'stump' (nullopt) when we split RPNs on a Constraint. · 2577b097
  Zuzana Baranová authored Oct 15, 2019
  
  2577b097
- smt: Silence a warning about missing braces in an initializer list. · 537cac1b
  Zuzana Baranová authored Oct 15, 2019
  
  537cac1b
- smt: Add some simple RPN and RPN decomposition unit tests. · 905f7bc9
  Zuzana Baranová authored Oct 15, 2019
  
  905f7bc9
Oct 14, 2019
- doc: Fix typos in documentation of divcc. · 319e6f04
  Zuzana Baranová authored Oct 14, 2019
  
  319e6f04
- smt: Simplify variable decomposition and reflect changes in union-find. · acf9b808
  Zuzana Baranová authored Oct 14, 2019
  
  acf9b808