Commits · 1b58e802d24129a4e1d36dc4ff71bdc720c96fec · paradise / mirror / DIVINE · GitLab

Jan 24, 2020
- smt: Add an extract::to_string() helper function. · 1b58e802
  Petr Rockai authored Jan 24, 2020
  
  1b58e802
- UI: Enable non-interactive mode if TRACE is set (instead of BRICK_TRACE). · 5d558e84
  Petr Rockai authored Jan 24, 2020
  
  5d558e84
- UI: If --symbolic is given, set the default LAMP config to 'symbolic'. · db11ba5c
  Petr Rockai authored Jan 24, 2020
  
  db11ba5c
- UI: Parse --lamp-config and pass it onto mc::Bitcode. · a6dcb034
  Petr Rockai authored Jan 24, 2020
  
  a6dcb034
- MC: Add support for a --lamp-config option to Bitcode. · dbc67e05
  Petr Rockai authored Jan 24, 2020
  
  dbc67e05
- RT: Add support for linking in a specified LAMP module. · ae1e5221
  Petr Rockai authored Jan 24, 2020
  
  ae1e5221
- smt: Raise an error if we try to decide feasibility without a solver. · 861151e8
  Petr Rockai authored Jan 24, 2020
  
  861151e8
- MC: Error out if we encounter marked pointers during explicit state comparison. · afea4969
  Petr Rockai authored Jan 24, 2020
  
  afea4969
- bricks: Remove the (now obsolete) brick-smt module. · 73e448b8
  Petr Rockai authored Jan 24, 2020
  
  73e448b8
- bricks: A few minor tweaks in brick-smtlib. · 6cdbbd45
  Petr Rockai authored Jan 24, 2020
  
  6cdbbd45
- bricks: Improve formatting (printing) of smt_atom_t values. · de6bd086
  Petr Rockai authored Jan 24, 2020
  
  de6bd086
- bricks: Add a formatting operator for smt_op. · c73562b5
  Petr Rockai authored Jan 24, 2020
  
  c73562b5
- bricks: Add a bw() [bitwidth] method to smt_atom_t. · 2f4b28a4
  Petr Rockai authored Jan 24, 2020
  
  2f4b28a4
- 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