Commits · 8f5cc719ec2cb74a3c71cc4e070d147c6937aa4b · paradise / mirror / DIVINE · GitLab

Jan 29, 2020
- 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
- lava: Add domain_mixin::fn_memcpy(). · d3ff22d2
  Petr Rockai authored Jan 26, 2020
  
  d3ff22d2
- lamp: Add support for fn_memcpy(). · c2f1cf88
  Petr Rockai authored Jan 26, 2020
  
  c2f1cf88
- lart: Re-enable memcpy lowering in DFA since now it mysteriously works. · 4e8386f3
  Petr Rockai authored Jan 26, 2020
  
  4e8386f3
- dios: Call destructors when moving data due to Array::insert(). · 572d17fb
  Petr Rockai authored Jan 26, 2020
  
  572d17fb
- lava: Rebuild mstring on top of new base classes and interfaces. · df9e991e
  Petr Rockai authored Jan 26, 2020
  
  df9e991e
- lava: Add missing bitwidth coercions to mstring::fn_strcmp(). · b3c4f755
  Petr Rockai authored Jan 26, 2020
  
  b3c4f755
- lava: Remove redundant uses of static_cast< bool >() in mstring. · a55fdf39
  Petr Rockai authored Jan 26, 2020
  
  a55fdf39
- lava: Cut down on copying 'constant' values. · 3d4f2174
  Petr Rockai authored Jan 26, 2020
  
  3d4f2174
- lava: Assert that all arguments of 'constant' ops have the same bitwidth. · 951a35fd
  Petr Rockai authored Jan 26, 2020
  
  951a35fd
- lamp: Advise caution when dealing with the coercion in semilattice::cast_one(). · f8f32c05
  Petr Rockai authored Jan 26, 2020
  
  f8f32c05
- lava: Add a (very unsafe) pointer access hatch to tagged_array. · ed79e020
  Petr Rockai authored Jan 26, 2020
  
  ed79e020
- lava: Add placeholders for string.h functions to domain_mixin. · a01aabf3
  Petr Rockai authored Jan 26, 2020
  
  a01aabf3
- lava: Add domain_mixin::op_{not,neg} placeholders. · 8be5ca8c
  Petr Rockai authored Jan 26, 2020
  
  8be5ca8c
- lava: By default, make each domain its own scalar and index domain. · ed9fc59a
  Petr Rockai authored Jan 26, 2020
  
  ed9fc59a
- lava: Fix domain_mixin::op_{gep,store}. · f4225a27
  Petr Rockai authored Jan 26, 2020
  
  f4225a27
- bricks: Replace forwarding with 'using' of base ctors in smt_expr. · a85174bb
  Petr Rockai authored Jan 26, 2020
  
  a85174bb
- lava: Properly call constructors & destructors in tagged_storage. · d74ef1c8
  Petr Rockai authored Jan 26, 2020
  
  d74ef1c8
- lava: Add a rudimentary term::op_gep() implementation. · 9e507657
  Petr Rockai authored Jan 26, 2020
  
  9e507657