silicon

silicon copied to clipboard

Use a Map from Snap to Snap to represent a magic wand snapshot.

1

@JonasAlaif and I are working on a different method to generate snapshots for magic wands. The problem with the current approach is that it is potentially unsound when we apply...

manud99

Previously, when Silicon could not use a provided trigger (because it could not evaluate at least one of the trigger expressions), - it could end up emitting a trigger containing...

marcoeilers

Function body is not available while checking the well-formedness of the postcondition

2

Contrary to carbon, it seems the function body/`result` is not available when establishing the well-formedness of the postcondition: ``` function require_true(x: Bool): Bool requires x { x } function f():...

pieter-bos

Debugging functionality implemented by @AndreaKe

marcoeilers

Multiple quantifiers to memory locations of same type

4

So this is not per se a bug report, more something I run into. I'm wondering if there are workarounds, or something fundamental what is needed here. For my research...

sakehl

I noticed that the GitHub workflow does not produce any useable output that can be analyzed. This makes it difficult to find out why some tests fail without running the...

manud99

Obviously true precondition "doesn't hold" when using predicate

1

The file below is a reduced version to highlight the problem: ``` function nonNull(): Ref ensures result != null function check(min_value1: Ref): Bool requires min_value1 != null predicate pred(nl: Ref)...

ArmborstL

Dspil

marcoeilers

This issue tracks all the tests that are ignored in the silicon test-suite that non deterministically time out. - all/third_party/stefan_recent/testTreeWandE1.vpr

Dspil