Commits · aa2e82e607a81767392008bd1d1979b956e8b27e · paradise / mirror / DIVINE · GitLab

Oct 10, 2019
- rst: Generate abstract store lifter templates. · aa2e82e6
  Henrich Lauko authored Oct 10, 2019
  
  aa2e82e6
Sep 04, 2019
- lart: Remove undesirable back propagation through phi nodes. · 289a640c
  Henrich Lauko authored Sep 04, 2019
  
  289a640c
Oct 18, 2019
- tools: Allow 'expect' declarations in divcheck that do not check result. · e9bbe172
  Adam Matoušek authored Oct 18, 2019
  
  e9bbe172
Oct 19, 2019
- smt: Remove former union-find.hpp (now part of brick-smt). · c4f10cc3
  Zuzana Baranová authored Oct 19, 2019
  
  c4f10cc3
- smt: Adapt RPN unit tests to changes in decompose(). · 344306ba
  Zuzana Baranová authored Oct 19, 2019
  
  344306ba
- bricks: Make union-find an (incremental) input-output parameter in decompose(). · 557098c4
  Zuzana Baranová authored Oct 19, 2019
  
  557098c4
- bricks: Add union-find to brick-smt (along with a unit test). · c710da83
  Zuzana Baranová authored Oct 19, 2019
  
  c710da83
- smt: Remove Unary & Binary from rpn.hpp (move to bricks). · 7975d295
  Zuzana Baranová authored Oct 19, 2019
  
  7975d295
- bricks: Add Unary & Binary to brick-smt (the *Op versions with added bitwidth). · 9cd0fb9e
  Zuzana Baranová authored Oct 19, 2019
  
  9cd0fb9e
- bricks: Move Operation, UnaryOp & BinaryOp out of RPNView into namespace token. · 7d3c6359
  Zuzana Baranová authored Oct 19, 2019
  
  7d3c6359
- smt: Remove decompose(), it has been moved into bricks. · ffc6cdca
  Zuzana Baranová authored Oct 19, 2019
  
  ffc6cdca
- bricks: Add decompose() to brick-smt, to split an RPN by dependent variables. · 7c56d231
  Zuzana Baranová authored Oct 19, 2019
  
  7c56d231
- MC: Fix build of t-machine.hpp. · 66455c50
  Petr Rockai authored Oct 19, 2019
  
  66455c50
- MC: Fix unit tests of the (somewhat obsolete) weaver-based Search class. · a063249b
  Petr Rockai authored Oct 19, 2019
  
  a063249b
- dios: A few style fixes in array.hpp. · e317f54d
  Petr Rockai authored Oct 19, 2019
  
  e317f54d
- VM: Ensure that value::full< T > is a compile-time constant. · 598c6a33
  Petr Rockai authored Oct 19, 2019
  
  598c6a33
- 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