Fix issue 651 #652
Merged
Fix issue 651 #652
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Dspil
approved these changes
May 12, 2023
koflin
added a commit
to koflin/gobra
that referenced
this pull request
Aug 18, 2023
commit caca746 Author: Felix Wolf <[email protected]> Date: Thu Aug 17 13:38:33 2023 +0200 Fix viperproject#668 (viperproject#669) commit f21fe70 Author: viper-admin <[email protected]> Date: Wed Aug 2 19:46:32 2023 +0200 Updates submodules (viperproject#667) Co-authored-by: ArquintL <[email protected]> commit 3590b3c Merge: 4a27390 04a7a2a Author: Linard Arquint <[email protected]> Date: Tue Jul 18 16:20:45 2023 +0200 Merge pull request viperproject#665 from viperproject/avoid-printing-asts Avoiding accidental printing of ASTs commit 04a7a2a Author: Linard Arquint <[email protected]> Date: Tue Jul 18 15:07:32 2023 +0200 adapts to avoid accidental printing of ASTs commit 4a27390 Merge: 8f9bfa7 a132190 Author: Linard Arquint <[email protected]> Date: Tue Jul 18 10:02:56 2023 +0200 Merge pull request viperproject#634 from viperproject/parallel-type-checking Parallelizing Gobra commit a132190 Merge: 716eeeb 4fc3cc9 Author: Linard Arquint <[email protected]> Date: Tue Jul 18 09:23:38 2023 +0200 Merges remote changes commit 716eeeb Author: Linard Arquint <[email protected]> Date: Tue Jul 18 09:23:21 2023 +0200 implements CR suggestions by Felix commit 4fc3cc9 Author: Linard Arquint <[email protected]> Date: Tue Jul 18 09:06:13 2023 +0200 Update src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala Co-authored-by: Felix Wolf <[email protected]> commit 8f9bfa7 Merge: 400015c 940a4b5 Author: Linard Arquint <[email protected]> Date: Tue Jul 18 08:18:36 2023 +0200 Merge pull request viperproject#664 from viperproject/auto-update-submodules Update Submodules commit 940a4b5 Author: ArquintL <[email protected]> Date: Mon Jul 17 17:36:04 2023 +0000 Updates submodules commit 400015c Merge: 1894cef 64389b2 Author: Linard Arquint <[email protected]> Date: Thu Jul 13 11:20:49 2023 +0200 Merge pull request viperproject#663 from viperproject/auto-update-submodules Update Submodules commit 64389b2 Author: ArquintL <[email protected]> Date: Thu Jul 13 07:54:42 2023 +0000 Updates submodules commit 1894cef Author: viper-admin <[email protected]> Date: Wed Jul 12 06:56:11 2023 +0200 Updates submodules (viperproject#661) Co-authored-by: jcp19 <[email protected]> commit 6e21fcf Merge: bb3610b ff48d9c Author: Linard Arquint <[email protected]> Date: Wed Jul 5 16:22:22 2023 +0200 Merges branch 'master' into 'parallel-type-checking' commit ff48d9c Merge: c56b335 d34ca31 Author: Linard Arquint <[email protected]> Date: Wed Jul 5 16:08:57 2023 +0200 Merge pull request viperproject#660 from viperproject/659-quantified-let-expressions-in-encoding-unsoundness Fix viperproject#659 commit d34ca31 Merge: 1929662 c56b335 Author: Linard Arquint <[email protected]> Date: Wed Jul 5 15:33:11 2023 +0200 Merges branch 'master' into '659-quantified-let-expressions-in-encoding-unsoundness' commit c56b335 Merge: 4393ad0 fc634a4 Author: Linard Arquint <[email protected]> Date: Wed Jul 5 15:32:22 2023 +0200 Merge pull request viperproject#658 from viperproject/auto-update-submodules Update Submodules commit 1929662 Author: Linard Arquint <[email protected]> Date: Tue Jul 4 09:30:59 2023 +0200 updates ViperServer to latest commit commit 3e87a6a Merge: 0fdf73a fc634a4 Author: Linard Arquint <[email protected]> Date: Tue Jul 4 08:58:25 2023 +0200 Merges branch 'auto-update-submodules' into '659-quantified-let-expressions-in-encoding-unsoundness' commit 0fdf73a Author: Linard Arquint <[email protected]> Date: Tue Jul 4 08:57:32 2023 +0200 adds failing test case commit fc634a4 Author: Linard Arquint <[email protected]> Date: Mon Jul 3 12:19:32 2023 +0200 fixes a compiler error caused by recent error reporting improvements commit d64f56a Author: Linard Arquint <[email protected]> Date: Mon Jul 3 12:05:30 2023 +0200 adapts regression tests to latest Viper changes commit 9772277 Author: Linard Arquint <[email protected]> Date: Mon Jul 3 12:03:33 2023 +0200 improves reporting of consistency errors and errors resulting from applying Viper transformers commit 08bfba3 Author: Linard Arquint <[email protected]> Date: Mon Jul 3 09:48:45 2023 +0200 adapts 'builtin' and 'stubs' packages to latest changes in Viper commit bb3610b Author: Linard Arquint <[email protected]> Date: Mon Jul 3 09:02:29 2023 +0200 fixes a typo commit a18c450 Author: ArquintL <[email protected]> Date: Sat Jul 1 06:00:52 2023 +0000 Updates submodules commit 50f379c Author: Linard Arquint <[email protected]> Date: Fri Jun 30 16:47:10 2023 +0200 fixes unit tests by making type-check caching specific to the config's choice of 32 or 64bit ints commit 52317a4 Author: Linard Arquint <[email protected]> Date: Fri Jun 30 15:48:17 2023 +0200 fixes compilation errors commit cda37bc Merge: 7f32830 4393ad0 Author: Linard Arquint <[email protected]> Date: Fri Jun 30 14:50:54 2023 +0200 Merges branch 'master' into 'pre-parse-unit-tests' commit 7f32830 Author: Linard Arquint <[email protected]> Date: Fri Jun 30 14:43:24 2023 +0200 cleanup commit e97cbf5 Author: Linard Arquint <[email protected]> Date: Fri Jun 30 11:22:00 2023 +0200 pre-parses and pre-typeChecks Gobra tests commit 6f41997 Author: Linard Arquint <[email protected]> Date: Fri Jun 30 09:51:57 2023 +0200 addresses several unit test errors commit 8d24c01 Author: Linard Arquint <[email protected]> Date: Thu Jun 29 17:02:23 2023 +0200 fixes compilation issue and undos parser caching for unit tests commit 046fe54 Author: Linard Arquint <[email protected]> Date: Thu Jun 29 16:43:04 2023 +0200 unifies job managers for parsing and type-checking and for the 3 modes commit 4393ad0 Author: viper-admin <[email protected]> Date: Wed May 31 20:13:50 2023 +0200 Updates submodules (viperproject#657) Co-authored-by: jcp19 <[email protected]> commit ed3aaf4 Author: Felix Wolf <[email protected]> Date: Wed May 31 20:13:16 2023 +0200 Fix viperproject#655 (viperproject#656) * Fix viperproject#655 * fixed reintroduced bug commit 5aa73b1 Author: viper-admin <[email protected]> Date: Fri May 19 15:45:09 2023 +0200 Updates submodules (viperproject#654) Co-authored-by: jcp19 <[email protected]> commit 5aeb8bf Author: viper-admin <[email protected]> Date: Tue May 16 12:02:56 2023 +0200 Updates submodules (viperproject#653) Co-authored-by: jcp19 <[email protected]> commit 178f985 Author: João Pereira <[email protected]> Date: Sun May 14 17:35:44 2023 +0200 Fix issue 651 (viperproject#652) * Add bug witness * Add fix * Reflect that the order of fields matter in the signature of AdtClauseT * use more general type commit 3ce34f3 Author: viper-admin <[email protected]> Date: Fri May 12 16:59:46 2023 +0200 Updates submodules (viperproject#650) Co-authored-by: jcp19 <[email protected]> commit c0e1c40 Author: João Pereira <[email protected]> Date: Thu May 11 19:50:47 2023 +0200 Update tutorial.md (viperproject#603) commit f4babde Author: viper-admin <[email protected]> Date: Fri May 5 18:38:26 2023 +0200 Updates submodules (viperproject#648) Co-authored-by: jcp19 <[email protected]> commit 686b53d Author: Linard Arquint <[email protected]> Date: Tue Mar 14 11:23:54 2023 +0100 Parses all inputs to 'GobraTests' in parallel before actually starting the unit tests commit c00c636 Author: Linard Arquint <[email protected]> Date: Thu Mar 30 14:02:13 2023 +0200 adds a sequential parser commit cfed2ce Author: Linard Arquint <[email protected]> Date: Thu Mar 30 09:50:34 2023 +0200 fixes reporting of errors in imported packages and reports them as part of type-checking commit 169d091 Author: Linard Arquint <[email protected]> Date: Wed Mar 15 19:46:48 2023 +0100 fixes parser error messages commit ba5f161 Author: Linard Arquint <[email protected]> Date: Tue Mar 14 17:59:26 2023 +0100 cleans up commit 3ed1598 Author: Linard Arquint <[email protected]> Date: Tue Mar 14 17:36:43 2023 +0100 fixes unit tests commit 66f542d Author: Linard Arquint <[email protected]> Date: Tue Mar 14 08:56:09 2023 +0100 Revert "restricts unit tests to 'regressions/features/header_only'" This reverts commit 53453f0. commit 9edc26e Author: Linard Arquint <[email protected]> Date: Tue Mar 14 08:54:47 2023 +0100 propagates parsing exceptions, built-in files are always considered even with enabled commit 53453f0 Author: Linard Arquint <[email protected]> Date: Mon Mar 13 14:21:29 2023 +0100 restricts unit tests to 'regressions/features/header_only' commit 04874c9 Author: Linard Arquint <[email protected]> Date: Fri Mar 10 16:02:12 2023 +0100 fixes a unit test commit a2b9b6c Author: Linard Arquint <[email protected]> Date: Fri Mar 10 15:43:46 2023 +0100 adds PPackage caching to parser commit a45f58c Author: Linard Arquint <[email protected]> Date: Thu Mar 9 15:12:10 2023 +0100 fixes license headers commit db26519 Author: Linard Arquint <[email protected]> Date: Thu Mar 9 15:10:54 2023 +0100 fixes license headers commit 5a4f353 Author: Linard Arquint <[email protected]> Date: Thu Mar 9 15:07:44 2023 +0100 fixes unit tests commit 81ea403 Author: Linard Arquint <[email protected]> Date: Thu Mar 9 09:38:03 2023 +0100 saves ongoing work commit 8039bcf Author: Linard Arquint <[email protected]> Date: Thu Mar 9 09:32:22 2023 +0100 updates ANTLR Go lexer and parser commit 62d6349 Author: Linard Arquint <[email protected]> Date: Sat Mar 4 20:22:55 2023 +0100 saves on-going work
koflin
added a commit
to koflin/gobra
that referenced
this pull request
Aug 18, 2023
commit caca746 Author: Felix Wolf <[email protected]> Date: Thu Aug 17 13:38:33 2023 +0200 Fix viperproject#668 (viperproject#669) commit f21fe70 Author: viper-admin <[email protected]> Date: Wed Aug 2 19:46:32 2023 +0200 Updates submodules (viperproject#667) Co-authored-by: ArquintL <[email protected]> commit 3590b3c Merge: 4a27390 04a7a2a Author: Linard Arquint <[email protected]> Date: Tue Jul 18 16:20:45 2023 +0200 Merge pull request viperproject#665 from viperproject/avoid-printing-asts Avoiding accidental printing of ASTs commit 04a7a2a Author: Linard Arquint <[email protected]> Date: Tue Jul 18 15:07:32 2023 +0200 adapts to avoid accidental printing of ASTs commit 4a27390 Merge: 8f9bfa7 a132190 Author: Linard Arquint <[email protected]> Date: Tue Jul 18 10:02:56 2023 +0200 Merge pull request viperproject#634 from viperproject/parallel-type-checking Parallelizing Gobra commit a132190 Merge: 716eeeb 4fc3cc9 Author: Linard Arquint <[email protected]> Date: Tue Jul 18 09:23:38 2023 +0200 Merges remote changes commit 716eeeb Author: Linard Arquint <[email protected]> Date: Tue Jul 18 09:23:21 2023 +0200 implements CR suggestions by Felix commit 4fc3cc9 Author: Linard Arquint <[email protected]> Date: Tue Jul 18 09:06:13 2023 +0200 Update src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala Co-authored-by: Felix Wolf <[email protected]> commit 8f9bfa7 Merge: 400015c 940a4b5 Author: Linard Arquint <[email protected]> Date: Tue Jul 18 08:18:36 2023 +0200 Merge pull request viperproject#664 from viperproject/auto-update-submodules Update Submodules commit 940a4b5 Author: ArquintL <[email protected]> Date: Mon Jul 17 17:36:04 2023 +0000 Updates submodules commit 400015c Merge: 1894cef 64389b2 Author: Linard Arquint <[email protected]> Date: Thu Jul 13 11:20:49 2023 +0200 Merge pull request viperproject#663 from viperproject/auto-update-submodules Update Submodules commit 64389b2 Author: ArquintL <[email protected]> Date: Thu Jul 13 07:54:42 2023 +0000 Updates submodules commit 1894cef Author: viper-admin <[email protected]> Date: Wed Jul 12 06:56:11 2023 +0200 Updates submodules (viperproject#661) Co-authored-by: jcp19 <[email protected]> commit 6e21fcf Merge: bb3610b ff48d9c Author: Linard Arquint <[email protected]> Date: Wed Jul 5 16:22:22 2023 +0200 Merges branch 'master' into 'parallel-type-checking' commit ff48d9c Merge: c56b335 d34ca31 Author: Linard Arquint <[email protected]> Date: Wed Jul 5 16:08:57 2023 +0200 Merge pull request viperproject#660 from viperproject/659-quantified-let-expressions-in-encoding-unsoundness Fix viperproject#659 commit d34ca31 Merge: 1929662 c56b335 Author: Linard Arquint <[email protected]> Date: Wed Jul 5 15:33:11 2023 +0200 Merges branch 'master' into '659-quantified-let-expressions-in-encoding-unsoundness' commit c56b335 Merge: 4393ad0 fc634a4 Author: Linard Arquint <[email protected]> Date: Wed Jul 5 15:32:22 2023 +0200 Merge pull request viperproject#658 from viperproject/auto-update-submodules Update Submodules commit 1929662 Author: Linard Arquint <[email protected]> Date: Tue Jul 4 09:30:59 2023 +0200 updates ViperServer to latest commit commit 3e87a6a Merge: 0fdf73a fc634a4 Author: Linard Arquint <[email protected]> Date: Tue Jul 4 08:58:25 2023 +0200 Merges branch 'auto-update-submodules' into '659-quantified-let-expressions-in-encoding-unsoundness' commit 0fdf73a Author: Linard Arquint <[email protected]> Date: Tue Jul 4 08:57:32 2023 +0200 adds failing test case commit fc634a4 Author: Linard Arquint <[email protected]> Date: Mon Jul 3 12:19:32 2023 +0200 fixes a compiler error caused by recent error reporting improvements commit d64f56a Author: Linard Arquint <[email protected]> Date: Mon Jul 3 12:05:30 2023 +0200 adapts regression tests to latest Viper changes commit 9772277 Author: Linard Arquint <[email protected]> Date: Mon Jul 3 12:03:33 2023 +0200 improves reporting of consistency errors and errors resulting from applying Viper transformers commit 08bfba3 Author: Linard Arquint <[email protected]> Date: Mon Jul 3 09:48:45 2023 +0200 adapts 'builtin' and 'stubs' packages to latest changes in Viper commit bb3610b Author: Linard Arquint <[email protected]> Date: Mon Jul 3 09:02:29 2023 +0200 fixes a typo commit a18c450 Author: ArquintL <[email protected]> Date: Sat Jul 1 06:00:52 2023 +0000 Updates submodules commit 50f379c Author: Linard Arquint <[email protected]> Date: Fri Jun 30 16:47:10 2023 +0200 fixes unit tests by making type-check caching specific to the config's choice of 32 or 64bit ints commit 52317a4 Author: Linard Arquint <[email protected]> Date: Fri Jun 30 15:48:17 2023 +0200 fixes compilation errors commit cda37bc Merge: 7f32830 4393ad0 Author: Linard Arquint <[email protected]> Date: Fri Jun 30 14:50:54 2023 +0200 Merges branch 'master' into 'pre-parse-unit-tests' commit 7f32830 Author: Linard Arquint <[email protected]> Date: Fri Jun 30 14:43:24 2023 +0200 cleanup commit e97cbf5 Author: Linard Arquint <[email protected]> Date: Fri Jun 30 11:22:00 2023 +0200 pre-parses and pre-typeChecks Gobra tests commit 6f41997 Author: Linard Arquint <[email protected]> Date: Fri Jun 30 09:51:57 2023 +0200 addresses several unit test errors commit 8d24c01 Author: Linard Arquint <[email protected]> Date: Thu Jun 29 17:02:23 2023 +0200 fixes compilation issue and undos parser caching for unit tests commit 046fe54 Author: Linard Arquint <[email protected]> Date: Thu Jun 29 16:43:04 2023 +0200 unifies job managers for parsing and type-checking and for the 3 modes commit 4393ad0 Author: viper-admin <[email protected]> Date: Wed May 31 20:13:50 2023 +0200 Updates submodules (viperproject#657) Co-authored-by: jcp19 <[email protected]> commit ed3aaf4 Author: Felix Wolf <[email protected]> Date: Wed May 31 20:13:16 2023 +0200 Fix viperproject#655 (viperproject#656) * Fix viperproject#655 * fixed reintroduced bug commit 5aa73b1 Author: viper-admin <[email protected]> Date: Fri May 19 15:45:09 2023 +0200 Updates submodules (viperproject#654) Co-authored-by: jcp19 <[email protected]> commit 5aeb8bf Author: viper-admin <[email protected]> Date: Tue May 16 12:02:56 2023 +0200 Updates submodules (viperproject#653) Co-authored-by: jcp19 <[email protected]> commit 178f985 Author: João Pereira <[email protected]> Date: Sun May 14 17:35:44 2023 +0200 Fix issue 651 (viperproject#652) * Add bug witness * Add fix * Reflect that the order of fields matter in the signature of AdtClauseT * use more general type commit 3ce34f3 Author: viper-admin <[email protected]> Date: Fri May 12 16:59:46 2023 +0200 Updates submodules (viperproject#650) Co-authored-by: jcp19 <[email protected]> commit c0e1c40 Author: João Pereira <[email protected]> Date: Thu May 11 19:50:47 2023 +0200 Update tutorial.md (viperproject#603) commit f4babde Author: viper-admin <[email protected]> Date: Fri May 5 18:38:26 2023 +0200 Updates submodules (viperproject#648) Co-authored-by: jcp19 <[email protected]> commit 686b53d Author: Linard Arquint <[email protected]> Date: Tue Mar 14 11:23:54 2023 +0100 Parses all inputs to 'GobraTests' in parallel before actually starting the unit tests commit c00c636 Author: Linard Arquint <[email protected]> Date: Thu Mar 30 14:02:13 2023 +0200 adds a sequential parser commit cfed2ce Author: Linard Arquint <[email protected]> Date: Thu Mar 30 09:50:34 2023 +0200 fixes reporting of errors in imported packages and reports them as part of type-checking commit 169d091 Author: Linard Arquint <[email protected]> Date: Wed Mar 15 19:46:48 2023 +0100 fixes parser error messages commit ba5f161 Author: Linard Arquint <[email protected]> Date: Tue Mar 14 17:59:26 2023 +0100 cleans up commit 3ed1598 Author: Linard Arquint <[email protected]> Date: Tue Mar 14 17:36:43 2023 +0100 fixes unit tests commit 66f542d Author: Linard Arquint <[email protected]> Date: Tue Mar 14 08:56:09 2023 +0100 Revert "restricts unit tests to 'regressions/features/header_only'" This reverts commit 53453f0. commit 9edc26e Author: Linard Arquint <[email protected]> Date: Tue Mar 14 08:54:47 2023 +0100 propagates parsing exceptions, built-in files are always considered even with enabled commit 53453f0 Author: Linard Arquint <[email protected]> Date: Mon Mar 13 14:21:29 2023 +0100 restricts unit tests to 'regressions/features/header_only' commit 04874c9 Author: Linard Arquint <[email protected]> Date: Fri Mar 10 16:02:12 2023 +0100 fixes a unit test commit a2b9b6c Author: Linard Arquint <[email protected]> Date: Fri Mar 10 15:43:46 2023 +0100 adds PPackage caching to parser commit a45f58c Author: Linard Arquint <[email protected]> Date: Thu Mar 9 15:12:10 2023 +0100 fixes license headers commit db26519 Author: Linard Arquint <[email protected]> Date: Thu Mar 9 15:10:54 2023 +0100 fixes license headers commit 5a4f353 Author: Linard Arquint <[email protected]> Date: Thu Mar 9 15:07:44 2023 +0100 fixes unit tests commit 81ea403 Author: Linard Arquint <[email protected]> Date: Thu Mar 9 09:38:03 2023 +0100 saves ongoing work commit 8039bcf Author: Linard Arquint <[email protected]> Date: Thu Mar 9 09:32:22 2023 +0100 updates ANTLR Go lexer and parser commit 62d6349 Author: Linard Arquint <[email protected]> Date: Sat Mar 4 20:22:55 2023 +0100 saves on-going work
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
When an
ADTClauseTis built, we first accumulate all the fields in a map from identifiers to the corresponding field type. However, this map does not preserve the order in which the fields are declared. In rare cases, the iteration order will actually differ from the order in which fields are declared, which can lead to ill-formed Viper programs being emited.