viperproject silicon issues

viperproject / silicon

Symbolic-execution-based verifier for the Viper intermediate verification language.

Mozilla Public License 2.0

79 stars 31 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Support for new assertin expressions

#875 marcoeilers opened 23 hours ago
0
Fixed accidental change in PR #863

#874 marcoeilers closed 1 week ago
0
Unfolding seems to be missing when asserting function

#873 bobismijnnaam closed 1 week ago
3
Fix macro transfer between verifiers in parallel branch verification

#872 marcoeilers closed 2 weeks ago
0
Avoid introducing MCE macros whose bodies are straightforward literals

#871 marcoeilers closed 3 weeks ago
0
Update download artifact

#870 marcoeilers closed 3 weeks ago
0
Update upload-artifact version

#869 marcoeilers closed 3 weeks ago
0
Confusing behaviour with `perm` in a quantifier for quantified vs non-quantified fields

#868 superaxander closed 3 weeks ago
2
Add block level messages

#867 trktby opened 4 weeks ago
0
Trying to fix silver build

#866 marcoeilers closed 1 month ago
0
Fixed pretty-printing of quantified chunks in debugger

#865 marcoeilers closed 1 month ago
0
Trying to fix Github issue

#864 marcoeilers closed 1 month ago
0
Basic verification debugging functionality

#863 marcoeilers closed 1 month ago
0
State merging failed: unexpected mismatch between symbolic states

#862 zgrannan opened 1 month ago
0
Questions about maintaining solver's context when adding parallelism in silicon

#861 fanweneddie closed 1 month ago
3
Consolidating quantified field and predicate chunks

#860 superaxander closed 3 weeks ago
5
Supporting MWSF in Z3 API

#859 marcoeilers closed 3 months ago
0
Function applications with `unfolding` not inferred to be equal

#858 bobismijnnaam closed 3 months ago
2
Trigger warning might cause slow and failing verification

#857 mschwerhoff opened 3 months ago
0
Incompleteness for heap-dependent functions with quantified permissions

#856 jwkai opened 3 months ago
3
Method only verifies with --useOldAxiomatization

#855 superaxander opened 3 months ago
0
Avoid computing join points when it's not required

#854 marcoeilers closed 3 months ago
0
Not pushing conditions using permission introspection further in

#853 marcoeilers closed 3 months ago
0
Recording constraints for newly-introduced variables during state consolidation

#852 marcoeilers closed 3 months ago
0
Lots of tests fail with --conditionalizePermissions

#851 marcoeilers opened 3 months ago
0
Weird behavior if WorkerBorrowingForkJoinWorkerThread.onStart throws an InterruptedException

#850 marcoeilers opened 3 months ago
0
Fix multiple `apply` of magic wands with quantified expressions

#849 manud99 opened 3 months ago
0
Add Inhaling expression

#848 manud99 opened 3 months ago
0
`FuncApp` in axioms

#847 pieter-bos opened 3 months ago
3
Fixing issue #845

#846 marcoeilers closed 3 months ago
0
Does not regonize heap dependent function as trigger

#845 sakehl closed 3 months ago
2
Unrelated fold removes knowledge of quantifier with predicate unside

#844 sakehl opened 3 months ago
2
Fixing issue #842

#843 marcoeilers closed 5 months ago
0
Unsoundness related to QPs with unsatisfiable conditions

#842 marcoeilers closed 5 months ago
2
Fixing error transformation for method call arguments

#841 marcoeilers closed 5 months ago
0
Make SM definitions non-global if necessary

#840 marcoeilers closed 5 months ago
0
Avoid making unnecessary summaries for individual quantified chunks

#839 marcoeilers closed 5 months ago
0
Verification Debugging in Silicon

#838 marcoeilers closed 1 month ago
0
Add test report to the GitHub actions workflow.

#837 manud99 opened 5 months ago
0
Use a Map from Snap to Snap to represent a magic wand snapshot.

#836 manud99 closed 3 months ago
3
Merge new QP chunks, assuming bounds and non-aliasing early.

#835 marcoeilers closed 5 months ago
0
Always use image functions for QPs

#834 marcoeilers closed 5 months ago
0
Unsound behavior with QPs without condition

#833 marcoeilers closed 5 months ago
0
Quantifier with predicates/predicates with quantifiers interfere with each other

#832 sakehl closed 5 months ago
4
Multiple quantifiers to memory locations of same type

#831 sakehl opened 5 months ago
4
Incorrect error message for method call on field access

#830 rayman2000 closed 5 months ago
3
More strictly constraining wildcards in MCE

#829 marcoeilers closed 6 months ago
0
Cleanup on new annotations and command line parameters

#828 marcoeilers closed 6 months ago
0
More fine-grained state consolidation configuration

#827 marcoeilers closed 6 months ago
0
Obviously true precondition "doesn't hold" when using predicate

#826 ArmborstL opened 6 months ago
1