Commits · 14dfcf12d919b5dc02f36e702f5311f32fbeab75 · paradise / mirror / DIVINE · GitLab

Jan 14, 2020
- rst: Allow make_term() to be called outside of the Term class. · 14dfcf12
  Petr Rockai authored Jan 14, 2020
  
  14dfcf12
- dios: Update KLEE platform glue re __vm_{peek,poke}. · f40086a3
  Petr Rockai authored Jan 14, 2020
  
  f40086a3
- dbg: Update the peek() call in Node::formula(). · a250aa47
  Petr Rockai authored Jan 14, 2020
  
  a250aa47
- rst: Update {peek,poke}_object to use the new __vm_{peek,poke} API. · c056c5a7
  Petr Rockai authored Jan 14, 2020
  
  c056c5a7
- rst: Use the updated __vm_poke interface to set up the __tainted value. · 5c179030
  Petr Rockai authored Jan 14, 2020
  
  5c179030
- VM: Add pointer (de)composition utilities to divm.h. · b175d94d
  Petr Rockai authored Jan 14, 2020
  
  b175d94d
- VM: Make the __vm_{peek,poke} hypercalls work with (address) ranges. · 6ebe72f2
  Petr Rockai authored Jan 14, 2020
  
  6ebe72f2
- mem: Change the peek/poke interface to be interval-based. · f7ce1924
  Petr Rockai authored Jan 14, 2020
  
  f7ce1924
- mem: Add an intersect() method to IntervalMetadataMap. · 5bb134aa
  Petr Rockai authored Jan 14, 2020
  
  5bb134aa
- mem: Make Loc default-constructible. · aecdd9ec
  Petr Rockai authored Jan 14, 2020
  
  aecdd9ec
- test: Add testcases for new __vm_{peek,poke} capabilities. · 8aed0fdf
  Petr Rockai authored Jan 14, 2020
  
  8aed0fdf
- test: Update __vm_{peek,poke} tests. · 361b622b
  Petr Rockai authored Jan 14, 2020
  
  361b622b
- rst: Do not overwrite the original term with its negation in constrain(). · ee767c44
  Petr Rockai authored Jan 14, 2020
  
  ee767c44
- VM: Generalize Eval::ptr2h() to also work with GenericPointer's directly. · 4a2f7e37
  Petr Rockai authored Jan 14, 2020
  
  4a2f7e37
- test: Fix the 'check klee' function. · 3e2e2325
  Petr Rockai authored Jan 14, 2020
  
  3e2e2325
- test: Fix propagation of the exit code from divcheck (again). · 61dcaf00
  Petr Rockai authored Jan 14, 2020
  
  61dcaf00
Jan 13, 2020
- releng: Show (non-vanilla) flavours in the HTML rendering of test results. · 21abe7c7
  Petr Rockai authored Jan 13, 2020
  
  21abe7c7
- test: Update the brick-{smt,smtlib} test list. · 99005f89
  Petr Rockai authored Jan 13, 2020
  
  99005f89
- test: Exclude a few problematic libc++ testcases from the 'klee' flavour. · 6aa0842c
  Petr Rockai authored Jan 13, 2020
  
  6aa0842c
- dios: Make the __dios_assert macro usable in C. · a2dac065
  Petr Rockai authored Jan 13, 2020
  
  a2dac065
- dios: Make assertion of debug mode into a platform-dependent hook. · 86e46d0f
  Petr Rockai authored Jan 13, 2020
  
  86e46d0f
- dios: Improve memory management in the KLEE port. · 10f39efa
  Petr Rockai authored Jan 13, 2020
  
  10f39efa
Dec 16, 2019
- test: Nothing guarantees that 'errno' is 0 at the start of main(). · 696141df
  Petr Rockai authored Dec 16, 2019
  
  696141df
Jan 13, 2020
- CC: Trace the cc1 arguments. · d7f0f52c
  Petr Rockai authored Jan 13, 2020
  
  d7f0f52c
- lart: Do not add leak checks after hypercall invocations, just function calls. · 3daef23b
  Petr Rockai authored Jan 13, 2020
  
  3daef23b
- test: Drop redundant chmod +x (make now takes care of it). · a06e2083
  Petr Rockai authored Jan 13, 2020
  
  a06e2083
- make: Ensure that scripts which are directly executed are actually executable. · 7a6000e1
  Petr Rockai authored Jan 13, 2020
  
  7a6000e1
- test: Fix a few problems with extraction of options from comments. · 76923b92
  Petr Rockai authored Jan 13, 2020
  
  76923b92
- libc: Streamline the cdefs.h function annotation macros a bit. · 6f24e5c0
  Petr Rockai authored Jan 13, 2020
  
  6f24e5c0
- test: Copy sources into the working directory if SKIP_CC is in effect. · 8c145807
  Petr Rockai authored Jan 13, 2020
  
  8c145807
- test: Update testcases which used verify -D to use -E. · b157f9a1
  Petr Rockai authored Jan 13, 2020
  
  b157f9a1
- UI: Make with_bc use -E for environment variables and -D for compiler defines. · 490d93af
  Petr Rockai authored Jan 13, 2020
  
  490d93af
- tools: Do not dump core when divcheck encounters an unexpected result. · ff17efb1
  Petr Rockai authored Jan 13, 2020
  
  ff17efb1
- test: Fix testcases spuriously passing when divcheck dies from a fatal signal. · f838b25a
  Petr Rockai authored Jan 13, 2020
  
  f838b25a
Jan 11, 2020
- MC: Fix infeasibility notification in (exhaustive) exec. · 55d41600
  Petr Rockai authored Jan 11, 2020
  
  55d41600
- test: Fail more verbosely in cmake-pthread.sh. · fef30810
  Petr Rockai authored Jan 11, 2020
  
  fef30810
- test: Propagate the exit code of divcheck if it fails (useful for timeouts). · 373b88ce
  Petr Rockai authored Jan 11, 2020
  
  373b88ce
- tools: Give divcheck a specific exit code for resource exhaustion. · b3be8e34
  Petr Rockai authored Jan 11, 2020
  
  b3be8e34
- bricks: Allow (shell) tests to indicate a timeout. · 3956fc17
  Petr Rockai authored Jan 11, 2020
  
  3956fc17
- bricks: Fix compilation of brick-{smt,smtlib}. · 06d3ef45
  Petr Rockai authored Jan 10, 2020
  
  06d3ef45