Commits · c0fd4e7cdba091a2e232ee7d3a849dd04a13645c · paradise / mirror / DIVINE · GitLab

Oct 11, 2019
- lart: Refactor function preprocessing in DFA. · c0fd4e7c
  Henrich Lauko authored Oct 11, 2019
  
  c0fd4e7c
Oct 10, 2019
- rst: Introduce lart intrinsic to access domain vtable. · 0cc2cf40
  Henrich Lauko authored Oct 10, 2019
  
  0cc2cf40
- lart: Generate function to allow access to domain vtable. · c979e544
  Henrich Lauko authored Oct 10, 2019
  
  c979e544
- lart: Fix annotation of thaw operation. · 40a1c566
  Henrich Lauko authored Oct 10, 2019
  
  40a1c566
- test: Add bunch of abstract unit aggregate tests. · 5b2a4c72
  Henrich Lauko authored Oct 10, 2019
  
  5b2a4c72
- lart: Implement generation of aggregate related lifters. · 5d79327b
  Henrich Lauko authored Oct 10, 2019
  
  5d79327b
- lart: Implement aggregate data flow analysis. · 50018c15
  Henrich Lauko authored Oct 10, 2019
  
  50018c15
- rst: Implement unit aggregate abstract domain. · 41f7bc67
  Henrich Lauko authored Oct 10, 2019
  
  41f7bc67
- rst: Fix interface annotation of term lifter. · b94009a6
  Henrich Lauko authored Oct 10, 2019
  
  b94009a6
- rst: Allow abstract constructors to take arguments. · 422ffb50
  Henrich Lauko authored Oct 10, 2019
  
  422ffb50
- rst: Create abstract aggregate constructor annotation. · 4fd6aee6
  Henrich Lauko authored Oct 10, 2019
  
  4fd6aee6
- rst: Generate abstract GEP lifter templates. · 4e725385
  Henrich Lauko authored Oct 10, 2019
  
  4e725385
- 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