Code

WIP: Iterator tracking issues#980

Code

Open

vl0w wants to merge 45 commits intoviperproject:masterviperproject/prusti-dev:masterfrom vl0w:iterators-feature-flagvl0w/prusti-dev:iterators-feature-flagCopy head branch name to clipboard

+1,047-315

Commits

Commits on Apr 28, 2022

• Adjust copy check in environment to better handle regions

  vl0w

  committed
  4caee3a

  Copy full SHA for 4caee3a

• Maybe we need to handle TyKind::Ref differently?

  vl0w

  committed
  ed7dffd

  Copy full SHA for ed7dffd

• Support associated types in copy check

  vl0w

  committed
  03b3640

  Copy full SHA for 03b3640

• Pass type with binder to type_is_copy to better account for regions

  vl0w

  committed
  138d98e

  Copy full SHA for 138d98e

• Normalize function signature in PureFunctionEncoder to account for associated types

  vl0w

  committed
  a408861

  Copy full SHA for a408861

• Remove check for validity of pure function in process_encoding_queue

  vl0w

  committed
  dbbed0d

  Copy full SHA for dbbed0d

• Erase all regions in copy check

  vl0w

  committed
  161b956

  Copy full SHA for 161b956

• Do not perform normalization when there are no projections

  vl0w

  committed
  eda1445

  Copy full SHA for eda1445

• Partially undo removal of code in process_encoding_queue.

  vl0w

  committed
  41aad37

  Copy full SHA for 41aad37

• Rename normalize_to, return original value if normalized value contains infer types

  vl0w

  committed
  e2a5467

  Copy full SHA for e2a5467

Commits on Apr 29, 2022

• Pass ParamEnv to resolve_assoc_types, make it fallible

  vl0w

  committed
  43a5387

  Copy full SHA for 43a5387

• Small cleanups

  vl0w

  committed
  b604cd4

  Copy full SHA for b604cd4

• Add custom iterator tests

  vl0w

  committed
  5dc9705

  Copy full SHA for 5dc9705

• Add flag to add experimental iterator support

  vl0w

  committed
  f8f2859

  Copy full SHA for f8f2859

• Move predicate normalization in constraint solver for better debugging

  vl0w

  committed
  0da3287

  Copy full SHA for 0da3287

• Do not copy preconditions of base spec to constrained spec

  vl0w

  committed
  c1cbead

  Copy full SHA for c1cbead

• Use predicate_must_hold_modulo_regions when resolving ghost constraints to account for references in associated types

  vl0w

  committed
  59bc78c

  Copy full SHA for 59bc78c

• Handle lifetimes in merge_generics

  vl0w

  committed
  0af45d7

  Copy full SHA for 0af45d7

Commits on May 2, 2022

• Support lifetimes in type models

  vl0w

  committed
  c527dc1

  Copy full SHA for c527dc1

• Relax needs_infer check in Environment::resolve_method_call to ignore non-resolved lifetimes

  vl0w

  committed
  c8081fb

  Copy full SHA for c8081fb

• Merge branch 'master' into iterators-feature-flag

  Show description for 78c51fb
  vl0w

  committed
  78c51fb

  Copy full SHA for 78c51fb

Commits on May 3, 2022

• Support lifetimes in type models

  vl0w

  committed
  af55da2

  Copy full SHA for af55da2

• Add first tests

  vl0w

  committed
  8c7a2ab

  Copy full SHA for 8c7a2ab

Commits on May 4, 2022

• Verification of Iter in while loop

  vl0w

  committed
  fa1c14a

  Copy full SHA for fa1c14a

• Create custom Copy/Clone impls for type models (do not derive them)

  vl0w

  committed
  5e396ff

  Copy full SHA for 5e396ff

• Adjust flag docs for iterator killswitch

  vl0w

  committed
  3afba7c

  Copy full SHA for 3afba7c

Commits on May 6, 2022

• Normalize substs in Environment::resolve_method_call to account for non-resolved associated types

  vl0w

  committed
  70e5b0f

  Copy full SHA for 70e5b0f

Commits on May 8, 2022

• Fix typo

  vl0w

  committed
  ed1a7a5

  Copy full SHA for ed1a7a5

Commits on May 10, 2022

• Support associated types in quantifiers

  vl0w

  committed
  d1d4953

  Copy full SHA for d1d4953

• Remove dead comment in any_type_needs_infer

  vl0w

  committed
  7e7bde4

  Copy full SHA for 7e7bde4

Commits on May 17, 2022

• Remove dead code

  vl0w

  committed
  e3bbbd9

  Copy full SHA for e3bbbd9

Commits on May 23, 2022

• Merge branch 'master' into iterators-feature-flag

  Show description for 8e05591
  vl0w

  committed
  8e05591

  Copy full SHA for 8e05591

Commits on May 30, 2022

• Merge branch 'master' into iterators-feature-flag

  Show description for 116bcd6
  vl0w

  committed
  116bcd6

  Copy full SHA for 116bcd6

Commits on Jun 12, 2022

• fix for viperproject#1033 with test cases

  

  Pointerbender

  authored and

  Aurel300

  committed
  f16f646

  Copy full SHA for f16f646

Commits on Jul 12, 2022

• snapshot equality

  Aurel300

  committed
  96ee8b9

  Copy full SHA for 96ee8b9

Commits on Jul 18, 2022

• remove special Fn*::call* treatment

  Aurel300

  committed
  414e081

  Copy full SHA for 414e081

• test closures using type-dependent contracts

  Aurel300

  committed
  2b6d632

  Copy full SHA for 2b6d632

Commits on Jul 19, 2022

• Merge remote-tracking branch 'upstream/master' into iterators-feature-flag

  Aurel300

  committed
  9142078

  Copy full SHA for 9142078

Commits on Jul 20, 2022

• fix

  Aurel300

  committed
  186e97e

  Copy full SHA for 186e97e

Commits on Jul 22, 2022

• Merge remote-tracking branch 'upstream/master' into iterators-feature-flag

  Aurel300

  committed
  8ed4eb2

  Copy full SHA for 8ed4eb2

Commits on Jul 27, 2022

• erase regions less eagerly for method calls

  Aurel300

  committed
  dbd4d2d

  Copy full SHA for dbd4d2d

• Merge remote-tracking branch 'upstream/master' into iterators-feature-flag

  Aurel300

  committed
  1eaa7d0

  Copy full SHA for 1eaa7d0

• fix

  Aurel300

  committed
  c74215b

  Copy full SHA for c74215b

Commits on Jul 29, 2022

• Merge remote-tracking branch 'upstream/master' into iterators-feature-flag

  Aurel300

  committed
  e9e5c78

  Copy full SHA for e9e5c78

• another unsafe core proof workaround for trait resolution

  Aurel300

  committed
  fa449f9

  Copy full SHA for fa449f9