Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion silicon
Submodule silicon updated 71 files
+2 −0 .gitignore
+1 −1 silver
+1 −0 src/main/resources/z3config.smt2
+23 −0 src/main/scala/Config.scala
+11 −11 src/main/scala/debugger/SiliconDebugger.scala
+4 −0 src/main/scala/interfaces/state/Chunks.scala
+29 −19 src/main/scala/logger/writer/SymbExLogReportWriter.scala
+141 −13 src/main/scala/reporting/Converter.scala
+1,157 −0 src/main/scala/reporting/SiliconResolvedCounterexample.scala
+3 −2 src/main/scala/rules/Brancher.scala
+50 −64 src/main/scala/rules/Evaluator.scala
+10 −2 src/main/scala/rules/ExecutionFlowController.scala
+107 −33 src/main/scala/rules/Executor.scala
+104 −43 src/main/scala/rules/HeapSupporter.scala
+35 −43 src/main/scala/rules/MagicWandSupporter.scala
+7 −3 src/main/scala/rules/MoreCompleteExhaleSupporter.scala
+2 −2 src/main/scala/rules/PredicateSupporter.scala
+488 −340 src/main/scala/rules/QuantifiedChunkSupport.scala
+106 −34 src/main/scala/rules/StateConsolidator.scala
+18 −2 src/main/scala/rules/SymbolicExecutionRules.scala
+37 −26 src/main/scala/state/Chunks.scala
+31 −12 src/main/scala/state/State.scala
+1 −3 src/main/scala/state/Utils.scala
+18 −0 src/main/scala/supporters/AnnotationSupporter.scala
+13 −0 src/main/scala/supporters/MethodSupporter.scala
+1 −3 src/main/scala/supporters/SnapshotSupporter.scala
+3 −3 src/main/scala/supporters/qps/PredicateAndWandSnapFunctionsContributor.scala
+10 −0 src/main/scala/verifier/DefaultMainVerifier.scala
+27 −4 src/main/scala/verifier/VerificationPoolManager.scala
+0 −13 src/test/resources/counterexamples/cyclic-ref.vpr
+0 −16 src/test/resources/counterexamples/functions.vpr
+0 −27 src/test/resources/counterexamples/lseg.vpr
+0 −19 src/test/resources/counterexamples/method-call.vpr
+0 −10 src/test/resources/counterexamples/negative.vpr
+0 −11 src/test/resources/counterexamples/permissions.vpr
+0 −27 src/test/resources/counterexamples/predicate.vpr
+0 −12 src/test/resources/counterexamples/ref-sequence.vpr
+0 −14 src/test/resources/counterexamples/sequence.vpr
+0 −27 src/test/resources/counterexamples/simple-refs-rec.vpr
+0 −21 src/test/resources/counterexamples/simple-refs.vpr
+78 −0 src/test/resources/greedyQP/array_sum.vpr
+57 −0 src/test/resources/greedyQP/qcomb_forall.vpr
+90 −0 src/test/resources/greedyQP/qcomb_independence.vpr
+50 −0 src/test/resources/greedyQP/qcomb_injectivity.vpr
+29 −0 src/test/resources/greedyQP/qp_access.vpr
+74 −0 src/test/resources/greedyQP/qp_arrays.vpr
+52 −0 src/test/resources/greedyQP/qp_assignments.vpr
+123 −0 src/test/resources/greedyQP/qp_bsearch.vpr
+40 −0 src/test/resources/greedyQP/qp_constraining_permissions.vpr
+71 −0 src/test/resources/greedyQP/qp_countfalse.vpr
+61 −0 src/test/resources/greedyQP/qp_dutch-flag.vpr
+194 −0 src/test/resources/greedyQP/qp_functions.vpr
+177 −0 src/test/resources/greedyQP/qp_generalised_shape.vpr
+123 −0 src/test/resources/greedyQP/qp_heap_dependent_triggers.vpr
+86 −0 src/test/resources/greedyQP/qp_issue_0102.vpr
+61 −0 src/test/resources/greedyQP/qp_issue_0184.vpr
+128 −0 src/test/resources/greedyQP/qp_issue_0205.vpr
+60 −0 src/test/resources/greedyQP/qp_misc1.vpr
+41 −0 src/test/resources/greedyQP/qp_repeated_reading.vpr
+50 −0 src/test/resources/greedyQP/qp_seqsingleelements.vpr
+53 −0 src/test/resources/greedyQP/qp_unbounded.vpr
+61 −0 src/test/resources/greedyQP/qpred_array.vpr
+110 −0 src/test/resources/greedyQP/qpred_exhale.vpr
+53 −0 src/test/resources/greedyQP/qpred_foralls.vpr
+33 −0 src/test/resources/greedyQP/qpred_injectivity.vpr
+67 −0 src/test/resources/greedyQP/qpred_partial_permissions.vpr
+86 −0 src/test/resources/greedyQP/qpred_permissions.vpr
+45 −0 src/test/resources/greedyQP/singleton_merging.vpr
+26 −0 src/test/scala/GeneralCounterexampleTests.scala
+6 −6 src/test/scala/MappedCounterexampleTests.scala
+21 −0 src/test/scala/SiliconTestsGreedyQP.scala
Loading