Jorge Navas
Jorge Navas
It seems that I need to create an instance of `ElfParser` from scratch and then I can read starting from section header `sh_offset` until `sh_size`.
This line https://github.com/fornwall/jelf/blob/master/src/main/java/net/fornwall/jelf/ElfRelocation.java#L55 only works if `EI_CLASS` is `CLASS_32`. If `EI_CLASS` is `CLASS_64` then the shift needs to be by 32.
Abstract domains only support arithmetic operations in three-address form (e.g., +,-,*,/) and addition of linear constraints. Abstract domains do not support addition of non-linear constraints. Moreover, linear constraints are simplified...
`adapt_sgraph.hpp` assumes that the graph weights are basic types. The assumption for basic types is because we use `memcpy` and `realloc` for efficiency reasons. Thus, to use bignums as weights...
_From @caballa on June 25, 2017 21:40_ A crab variable can contain a pointer (e.g., crab-llvm stores `Value*` in a crab variable and seahorn stores `Expr`). This is very useful...
- [ ] widening with thresholds - [ ] narrowing - [x] strict inequalities for integers - [x] disequations (similar precision as intervals) _From @caballa on October 15, 2016 23:33_...
_From @caballa on October 15, 2016 23:18_ For intervals and zones, we need at least: - make sure rounding is correct (e.g., if upper bounds towards +oo, etc) - make...
It requires to implement `make_thresholds` in `apron_domains.hpp`. There are at least two examples: - `tests/domains/test2-rat.cc` - `tests/domains/test3-rat.cc` that would be benefit.
The current assumption is that an external call cannot allocate memory or unify pointers. If the external call returns a pointer, the address is a non-deterministic value. We propose to...