Marco Eilers
Marco Eilers
I'm trying out a change in Silicon that speeds this example up by quite a bit (PR #835) by essentially assuming non-aliasing information for QPs earlier. For me, the version...
Yes, there is at least one part of Silicon's QP handling that is inherently quadratic in the number of snapshot maps Silicon generates, that seems to be the issue here...
Couldn't we trigger on the stateless version of the function in that case?
Warnings, at least some kinds (see for example this https://github.com/viperproject/silicon/blob/228387ad9fd600171dfc9fa98b0a24e93acdc482/src/main/scala/verifier/DefaultMainVerifier.scala#L160) are shown in the IDE.
We now emit warnings for this, so it's no longer *silently* ignored.
There seem to be multiple issues: - Silicon seems to spend the vast majority of its time proving that it has permission to the ``arr_int`` and ``int`` fields read in...
The snapshot map cache fix by itself seems to cut verification time roughly in half.
I would consider this intentional behavior, especially now that Viper has opaque functions, which means that for individual function applications, the function body may not be known to the verifier....
> @marcoeilers Does Silicon encode `assert ; ...` to some SMT2 where `` is repeated twice, with a pop in between? It does this for assertions that are directly asserted...
I hoped it would, but it actually leads to worse performance on SCION code. So for now I basically just wanted to have this option available to experiment with.