Commits · b38c1d3f64d58ef5c87ebaac049ad84bca80a2f0 · paradise / mirror / DIVINE · GitLab

SCHEDULED DOWNTIME: GitLab's virtual host must be rebooted to apply security updates. The reboot will occur on Monday, 2024-05-06, between 03:45 and 4:00 AM.

Jan 28, 2020
- MC: Load mcsema option from report. · b38c1d3f
  Lukáš Korenčik authored Jan 28, 2020
  
  b38c1d3f
- cmake: Add divine-ra as library. · ee7bdee9
  Lukáš Korenčik authored Jan 28, 2020
  
  ee7bdee9
Jan 21, 2020
- UI: Add refine as subcommand. · 9aed14ca
  Lukáš Korenčik authored Jan 21, 2020
  
  9aed14ca
- ra: Die if a boot error is encountered. · 383a22d8
  Lukáš Korenčik authored Jan 21, 2020
  
  383a22d8
- ra: Add report method. · b439b237
  Lukáš Korenčik authored Jan 21, 2020
  
  b439b237
- lart: Add methods that return info about current state of rewire_calls pass. · 193b2977
  Lukáš Korenčik authored Jan 21, 2020
  
  193b2977
- ra: Add two simple testcases for rewire calls refinement. · 3e0ffcc1
  Lukáš Korenčik authored Jan 21, 2020
  
  3e0ffcc1
- ra: Move parts of llvmrefine to cpp file. · 1172cb61
  Lukáš Korenčik authored Jan 21, 2020
  
  1172cb61
- ra: Add ctor that accepts llvm objects that are already created. · 2d73a429
  Lukáš Korenčik authored Jan 21, 2020
  
  2d73a429
- ra: Reflect API change of rewirecalls pass. · d2c3453f
  Lukáš Korenčik authored Jan 21, 2020
  
  d2c3453f
Jan 20, 2020
- ra: Add extra layer between llvm_refinement and underlying llvm pass. · 258aec30
  Lukáš Korenčik authored Jan 20, 2020
  
  258aec30
- ra: Remove obsolete remnants of get_ce_t. · e512ed10
  Lukáš Korenčik authored Jan 20, 2020
  
  e512ed10
- ra: Parametrize stack trace with lambda. · e944ff30
  Lukáš Korenčik authored Jan 20, 2020
  
  e944ff30
- ra: Give counter-example accessor a state. · a0212386
  Lukáš Korenčik authored Jan 20, 2020
  
  a0212386
- ra: Add method that returns stack trace of counter-example. · 71915398
  Lukáš Korenčik authored Jan 20, 2020
  
  71915398
Jan 21, 2020
- lart: Rename pass to rewirecalls and fix codestyle. · 95b45ace
  Lukáš Korenčik authored Jan 21, 2020
  
  95b45ace
Jan 19, 2020
- ra: Add basic draft of how refinement may look like. · 1b31a756
  Lukáš Korenčik authored Jan 19, 2020
  
  1b31a756
Jan 31, 2020
- bricks: Optimize the brick-smt code for cases when it runs in DiVM. · 81ca492c
  Petr Rockai authored Jan 31, 2020
  
  81ca492c
- smt: Use the caching solver variants by default. · 81d854e9
  Petr Rockai authored Jan 31, 2020
  
  81d854e9
- smt: Update and improve the 'caching' solver variant. · 7a73a980
  Petr Rockai authored Jan 31, 2020
  
  7a73a980
Jan 29, 2020
- bricks: Make the atomicity check compile for types with non-trivial copying. · 04d8948c
  Petr Rockai authored Jan 29, 2020
  
  04d8948c
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