Commits · 26fdfeb13dae183a1e8903a0465673ab7af9f5cd · paradise / mirror / DIVINE · GitLab

Jan 24, 2020
- bricks: Add value() and bounds() to smt_atom_t (for use with relevant ops). · 26fdfeb1
  Petr Rockai authored Jan 24, 2020
  
  26fdfeb1
- bricks: Add a bunch of convenient is_* predicates to smt_atom_t. · 3a6aca6b
  Petr Rockai authored Jan 24, 2020
  
  3a6aca6b
- bricks: Fix construction of non-var smt_atom instances with immediate storage. · adfe9002
  Petr Rockai authored Jan 24, 2020
  
  adfe9002
- bricks: Add an smt_arity( smt_op ) convenience function. · 307bb9bf
  Petr Rockai authored Jan 24, 2020
  
  307bb9bf
- bricks: Rename the (misleading) smt_op::{var,const}_bool to {var,const}_i1. · b90bf37b
  Petr Rockai authored Jan 24, 2020
  
  b90bf37b
- bricks: The result of smt_op::bv_not is always a single bit. · d46724b2
  Petr Rockai authored Jan 24, 2020
  
  d46724b2
- bricks: Tag the SMT operators '=' and '!=' as comparisons. · 2561914f
  Petr Rockai authored Jan 24, 2020
  
  2561914f
- bricks: Fix smt_expr::apply( smt_expr ). · c737bf50
  Petr Rockai authored Jan 24, 2020
  
  c737bf50
- bricks: Add a missing bool_not operator to smt_op. · b81e9e89
  Petr Rockai authored Jan 24, 2020
  
  b81e9e89
- test: Skip leak checks for abstract (but non-symbolic) testcases. · c0f20e24
  Petr Rockai authored Jan 24, 2020
  
  c0f20e24
- test: Update 'sym' testcases to use the new __lamp_* APIs. · 3d5cc20f
  Petr Rockai authored Jan 24, 2020
  
  3d5cc20f
- test: Update tests for the 'constant' abstract domain. · 5d753812
  Petr Rockai authored Jan 24, 2020
  
  5d753812
- test: Do a basic sanity check of abstraction and the __lamp_any_* functions. · c5dca043
  Petr Rockai authored Jan 24, 2020
  
  c5dca043
- VM: Allow getelementptr to affect the entire pointer, not just the offset. · a1f129ef
  Petr Rockai authored Jan 24, 2020
  
  a1f129ef
Jan 16, 2020
- lart: Fix lowering of memcpy in the DFA preprocessing pass. · 546242f3
  Henrich Lauko authored Jan 16, 2020
  
  546242f3
Jan 23, 2020
- bricks: Fix the bitwidth of the result of SMT equality and inequality ops. · db1aef9f
  Petr Rockai authored Jan 23, 2020
  
  db1aef9f
- bricks: Add a 'comparison' operator category to smt_traits(). · 660a8cdf
  Petr Rockai authored Jan 23, 2020
  
  660a8cdf
- bricks: Distinguish between resizing and width-preserving SMT casts. · 6b33b7f4
  Petr Rockai authored Jan 23, 2020
  
  6b33b7f4
- bricks: Rebase brick-smtlib on top of brick-nusmt and update the API. · 05be604f
  Petr Rockai authored Jan 23, 2020
  
  05be604f
Jan 18, 2020
- lamp: Rename the lift_one_X domain operations to lift_X. · 3bd2a535
  Petr Rockai authored Jan 18, 2020
  
  3bd2a535
- lamp: Update the 'trivial' (only constants and unit) metadomain. · 4587b0a4
  Petr Rockai authored Jan 17, 2020
  
  4587b0a4
- cmake: Build bitcode modules from dios/lamp. · bf856b2d
  Petr Rockai authored Jan 17, 2020
  
  bf856b2d
- lamp: Make semilattice.hpp build and use new lamp/lava conventions. · 31cf1bce
  Petr Rockai authored Jan 17, 2020
  
  31cf1bce
- lamp: Fix compilation of 'wrapper.hpp'. · 9f53c0f0
  Petr Rockai authored Jan 17, 2020
  
  9f53c0f0
Jan 20, 2020
- lart: Remove abstract domain and operation indexing code. · 65d5f9e1
  Petr Rockai authored Jan 20, 2020
  
  65d5f9e1
Jan 18, 2020
- lamp: Move the semilattice metadomain from rst into lamp. · 5809667e
  Petr Rockai authored Jan 17, 2020
  
  5809667e
- libc: Use __lamp_any_* instead of __sym_val_* for __VERIFIER_*. · 7485462c
  Petr Rockai authored Jan 17, 2020
  
  7485462c
- lamp: Add an (initial) README. · 09feed38
  Petr Rockai authored Jan 17, 2020
  
  09feed38
Jan 17, 2020
- lamp: Add a first iteration of a C-style interface for LART. · b3bfefb6
  Petr Rockai authored Jan 17, 2020
  
  b3bfefb6
- dios: Add 'lamp', a collection of abstract metadomains. · 7f739a15
  Petr Rockai authored Jan 17, 2020
  
  7f739a15
Jan 19, 2020
- rst: Resolve conflicts in domains.h and mstring.cpp (both have been deleted). · 6051aa6e
  Petr Rockai authored Jan 19, 2020
  
  6051aa6e
Jan 16, 2020
- test: Resurrect mstring tests. · d4d72e2f
  Henrich Lauko authored Jan 16, 2020
  
  d4d72e2f
- rst: Instantiate hybrid mstring from the symbolic and constant domain. · 2d4e9fdb
  Henrich Lauko authored Jan 16, 2020
  
  2d4e9fdb
- rst: Implement mstring abstract constructors. · 18caa6d5
  Henrich Lauko authored Jan 16, 2020
  
  18caa6d5
- rst: Add subtraction to the mstring domain. · dca0eeb5
  Henrich Lauko authored Jan 16, 2020
  
  dca0eeb5
- rst: Fix mstring strcmp. · 3d9d63e5
  Henrich Lauko authored Jan 16, 2020
  
  3d9d63e5
- rst: Invoke explicitly to bool conversion in the mstring implementation. · 39195936
  Henrich Lauko authored Jan 16, 2020
  
  39195936
- rst: Make mstring segment iterators more sane. · 57c103e7
  Henrich Lauko authored Jan 16, 2020
  
  57c103e7
- rst: Extend all bounds of mstring to 64-bit integer. · 7c95f952
  Henrich Lauko authored Jan 16, 2020
  
  7c95f952
Dec 15, 2019
- rst: Instantiate missing mstring operations. · 912332ff
  Henrich Lauko authored Dec 15, 2019
  
  912332ff