Commits · 9823252aef4588b3a05db7a51fe8cdf6a85ac2ee · paradise / mirror / DIVINE · GitLab

Jan 26, 2020
- dios: Coax the compiler to produce slightly better code for Array. · 9823252a
  Petr Rockai authored Jan 26, 2020
  
  9823252a
Jan 31, 2020
- UI: Include SMT, DiVM and hashing cycle timers in the detailed YAML report. · e721e668
  Petr Rockai authored Jan 31, 2020
  
  e721e668
- MC: Add timers for state hashing and for DiVM computation. · f0dbc1ef
  Petr Rockai authored Jan 31, 2020
  
  f0dbc1ef
- smt: Add timers for solver calls (separate for equality and for feasibility). · 12f938c6
  Petr Rockai authored Jan 31, 2020
  
  12f938c6
- bricks: Add an implementation of a low-overhead, tsc-based profiling timer. · 2dc2809a
  Petr Rockai authored Jan 31, 2020
  
  2dc2809a
- bricks: Remove the unused smt_op::constraint pseudo-operation. · 9db4ee84
  Petr Rockai authored Jan 31, 2020
  
  9db4ee84
Jan 30, 2020
- smt: Get rid of brq::smt_op::constraint. · d0e10929
  Petr Rockai authored Jan 30, 2020
  
  d0e10929
- dios: Compile librst and lamp configs with -O3. · e11b6060
  Petr Rockai authored Jan 30, 2020
  
  e11b6060
- bricks: Fix union_find::make_set in the case the key already exists. · c7397b46
  Petr Rockai authored Jan 30, 2020
  
  c7397b46
- rst: Write hand-optimized code for term::assume(). · 604d2c6a
  Petr Rockai authored Jan 30, 2020
  
  604d2c6a
- lava: Flip back to using a dense_map for the decomposed path condition. · b56c03a1
  Petr Rockai authored Jan 30, 2020
  
  b56c03a1
- smt: Ignore empty components of the path condition. · 97edd4ea
  Petr Rockai authored Jan 30, 2020
  
  97edd4ea
Jan 29, 2020
- cmake: Make sure we have pandoc-crossref before building documentation. · 2be63c4a
  Vladimír Štill authored Jan 29, 2020
  
  2be63c4a
Jan 30, 2020
- VM: Translate peek/poke offsets between user and internal representations. · e21a7998
  Petr Rockai authored Jan 30, 2020
  
  e21a7998
Jan 29, 2020
- bricks: Reduce the runtime overhead of brq::smt_op_traits(). · f3aa133b
  Petr Rockai authored Jan 29, 2020
  
  f3aa133b
- bricks: Make dense_map behave more like std::map for erased/missing elements. · 6aa6e0ff
  Petr Rockai authored Jan 29, 2020
  
  6aa6e0ff
- test: Update the list of bricks unit tests. · 551761d6
  Petr Rockai authored Jan 29, 2020
  
  551761d6
- bricks: Allow instances of brq::hash_table for types with destructors. · 1a6ae89e
  Petr Rockai authored Jan 29, 2020
  
  1a6ae89e
- test: Tag a few more product-lines testcases with z3skip. · 8f5cc719
  Petr Rockai authored Jan 29, 2020
  
  8f5cc719
- mem: Fix an off-by-one in an assertion of hint validity in Data::make. · 2f5c5d9c
  Petr Rockai authored Jan 29, 2020
  
  2f5c5d9c
- cmake: Fix finding python in libc++ build. · 19a155cb
  Vladimír Štill authored Jan 29, 2020
  
  19a155cb
- dios: Add a missing file to libc++. · 0259a8c0
  Vladimír Štill authored Jan 29, 2020
  
  0259a8c0
- lart: Fix compilation of abstract/test.h. · d2908f19
  Petr Rockai authored Jan 29, 2020
  
  d2908f19
- test: Tamper currently only works if --lamp-config is in effect. · 9d21d993
  Petr Rockai authored Jan 29, 2020
  
  9d21d993
- sim: Fix fallout (broken 'tamper') from the recent abstract domain refactor. · f08e306e
  Petr Rockai authored Jan 29, 2020
  
  f08e306e
Jan 26, 2020
- lava: Update the brick-smt #include. · 646aae6b
  Petr Rockai authored Jan 26, 2020
  
  646aae6b
- smt: Update the brick-smt #include. · 1f7c32fc
  Petr Rockai authored Jan 26, 2020
  
  1f7c32fc
- bricks: Rename brick-nusmt back to brick-smt now that it works. · e7a720b4
  Petr Rockai authored Jan 26, 2020
  
  e7a720b4
- test: Update the list of bricks unit tests. · fd7e394a
  Petr Rockai authored Jan 26, 2020
  
  fd7e394a
- test: Fix the brick-update script. · 1b9d0155
  Petr Rockai authored Jan 26, 2020
  
  1b9d0155
- test: Fix a copy-pasta buffer overflow in mstring-null-termination. · 33f88097
  Petr Rockai authored Jan 26, 2020
  
  33f88097
- lamp: Cut down on the runtime overhead of __lamp_* wrappers. · ac63fd3e
  Petr Rockai authored Jan 26, 2020
  
  ac63fd3e
- lamp: Sprinkle __inline around semilattice to flatten the abstraction tower. · 6450bf1c
  Petr Rockai authored Jan 26, 2020
  
  6450bf1c
- smt: Fix argument order in Z3::constant(). · cf474e3d
  Petr Rockai authored Jan 26, 2020
  
  cf474e3d
- lamp: Add semilattice::op_zfit(). · 8e37d3e5
  Petr Rockai authored Jan 26, 2020
  
  8e37d3e5
- lava: Add a fake 'zfit' operation to mstring. · 1f641b5c
  Petr Rockai authored Jan 26, 2020
  
  1f641b5c
- lava: Fix memcpy() support in mstring. · 566958cd
  Petr Rockai authored Jan 26, 2020
  
  566958cd
- lart: Fix the definition of type_onion::maybe_aggregate(). · 8b43cf0a
  Petr Rockai authored Jan 26, 2020
  
  8b43cf0a
- test: Run basic mstring tests in both symbolic- and constant-based configs. · ac125adc
  Petr Rockai authored Jan 26, 2020
  
  ac125adc
- test: Cut the mstring null termination test in half. · 46ae169e
  Petr Rockai authored Jan 26, 2020
  
  46ae169e