Commits · fe49e63c0c75eaace2b72418688f03575a89050f · paradise / mirror / DIVINE · GitLab

Jan 24, 2020
- lamp: Add 'assume' (constraints) and 'decide' (conditional branching). · fe49e63c
  Petr Rockai authored Jan 24, 2020
  
  fe49e63c
- lamp: Add __lamp_freeze() and __lamp_melt() to wrapper.hpp. · 32d39a0e
  Petr Rockai authored Jan 24, 2020
  
  32d39a0e
- lamp: Add __lamp_any_* wrappers (for creating undetermined values). · 0cbb2260
  Petr Rockai authored Jan 24, 2020
  
  0cbb2260
- lamp: Add a header that describes the C interface (as sys/lamp.h). · 700f0807
  Petr Rockai authored Jan 24, 2020
  
  700f0807
- lamp: Split 'wrap' (returns a pointer) from 'lift' (returns a tainted scalar). · 45210334
  Petr Rockai authored Jan 24, 2020
  
  45210334
- lart: Put code for inheriting metadata back into the tainting pass. · 618bc23a
  Petr Rockai authored Jan 24, 2020
  
  618bc23a
- lart: Add a metadata tag for 'faultable' function calls. · 38d96d9c
  Petr Rockai authored Jan 24, 2020
  
  38d96d9c
- lart: A few minor style fixes under abstract/. · 878c10dc
  Petr Rockai authored Jan 24, 2020
  
  878c10dc
- lart: Update add_meta() calls in the DFA pass. · 9b5bf2d8
  Petr Rockai authored Jan 24, 2020
  
  9b5bf2d8
- lart: Attach LAMP operations as metadata to instructions to be abstracted. · 0739dadb
  Petr Rockai authored Jan 24, 2020
  
  0739dadb
- lart: Allow function pointers to be stashed in metadata. · e090c110
  Petr Rockai authored Jan 24, 2020
  
  e090c110
- lart: Get rid of domain indices in the Synthesize pass. · aa3f6bca
  Petr Rockai authored Jan 24, 2020
  
  aa3f6bca
- lart: Remove the InitAbstractions pass (responsible for identifying domains). · 657f1372
  Petr Rockai authored Jan 24, 2020
  
  657f1372
- bricks: Prevent constructor calls when bitcasting from non-trivial types. · 022a06e7
  Petr Rockai authored Jan 24, 2020
  
  022a06e7
- dbg: Fix a segfault in Context::is_same(), plus a style fix. · b0290bb4
  Petr Rockai authored Jan 24, 2020
  
  b0290bb4
- dbg: Use smt::extract::to_string() instead of a locally grown variant thereof. · 44e974a4
  Petr Rockai authored Jan 24, 2020
  
  44e974a4
- MC: Replace copy-pasta with smt::extract::to_string(). · f9d5ec60
  Petr Rockai authored Jan 24, 2020
  
  f9d5ec60
- 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