Michael Emmi
Michael Emmi
Here’s a fun piece of code that we cannot handle at all. ``` #include #include int main() { __m128i A = _mm_set_epi32(13,12,11,10); __m128i B = _mm_set_epi32(23,22,21,20); A = _mm_shuffle_epi32(A,2*1 +...
The following [array_forall](https://github.com/smackers/smack/blob/develop/test/contracts/array_forall.c) example fails for a very silly reason having to do with quantifier instantiation: slight variations of the quantified expressions in the produced Boogie code — e.g., inlining...
(from Shaobo) There is obviously a scalability issue of SMACK when it is applied on DeviceDriver64 category of SVCOMP benchmarks that requires reasoning about bit-vectors. I think it would be...
Please examine each of the following points so that we can help you as soon and best as possible. **Describe the bug** The call graph computed by Spark’s implementation of...
The current usage examples use old versions of d3-graphviz. For example, e.g., [d3-graphviz Basic example](https://gist.github.com/magjac/a23d1f1405c2334f288a9cca4c0ef05b) uses 3.0.5. There’s been a breaking change since then, from 4.5.x to 5.x, and I...
Proving the postcondition below seems to require expressing that `f1` and `f2` return true if and only if some element of `a1` and `a2` respectively are greater than zero. ```solidity...
``` $ cat a.sol && solc-verify.py a.sol pragma solidity ^0.5.0; contract A { /// @notice postcondition address(this).balance >= __verifier_old_uint(address(this).balance) function f1() public payable { } } A::f1: ERROR - a.sol:6:5:...
I expected the following to work: ``` $ cat a.sol && solc-verify.py a.sol ``` ```solidity pragma solidity ^0.5.0; /// @notice invariant __verifier_eq(a1, a2) contract C { int[] a1; int[] a2;...
It seems that overriding an inherited virtual function causes a crash! Not clear whether this is something you want to deal with, since (a) this example also crashes `solc`, and...
It’s not clear how we can state postconditions for functions which update storage with memory-typed arguments, as in the following example: ``` $ cat a.sol && solc-verify.py a.sol pragma solidity...