Many small updates #154

marcoeilers · 2023-08-21T20:31:25Z

Viper 23.07
Script for nagini_client
Removed SplitOn (no longer needes because of Silicon's --parallelizeBranches)
Added viper_arg
Added ToMS, Forall_n
Added Refute, Decreases
Supporting AnnAssign
Using ViperFrontendAPI
New dict encoding using Viper maps
Better counterexamples for generic classes
SecC examples

This change is

…elizeBranches

…t script

marcoeilers and others added 21 commits December 6, 2022 14:46

Silicon works with new Viper version, removed SplitOn, enabled parall…

09014fc

…elizeBranches

Using Viper maps for dicts, counterexamples still TODO

eb6a5c8

Carbon args, assuming injectivity, adapted Carbon test annotations

7a0716d

Tiny changes to make SIF work

4ac6c4f

Updated included Viper version

a260601

Added missing secc examples + VerifyThis example

4b6500f

Updated Silicon, added Silicon option

a98e5ed

Merge branch 'master' into update_01_23

5f71464

Foralln, toMS, new Viper, counterexamples for generics

6edae35

Update Boogie version

5e31e7a

Fixed backend options

18d3626

Adapted test annotations

ef9e7fa

Added test for ToMS

bea39a0

Removed SplitOn, fixed MustRelease CE crash

1ba07fe

Supporting AnnAssigns

616d5e7

Fixing two bugs

da690fa

Viper 23.07 support, Refute, Decreases

5465319

Updated Carbon, fixed CE issue, exhaleMode 2

a68a698

Fixing some tests

33daa3c

Fixed more tests, more extensionality, viper_args, refute test, clien…

e367ff8

…t script

Fixing issues in the backend

707855d

marcoeilers changed the title ~~Big update~~ Many small updates Aug 22, 2023

Fixed Silicon issue

bc8cc0f

marcoeilers merged commit 362ee73 into master Aug 22, 2023
2 checks passed

marcoeilers deleted the update_01_23 branch August 22, 2023 17:21

Provide feedback