Skip to content

Commit

Permalink
Squashed commit of the following:
Browse files Browse the repository at this point in the history 
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
  • Loading branch information
@koflin
koflin committed Aug 18, 2023
1 parent ed2d5a7 commit 948b641
Show file tree
Hide file tree
Showing 5 changed files with 17 additions and 2 deletions.
1 change: 1 addition & 0 deletions build.sbt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ lazy val gobra = (project in file("."))
libraryDependencies += "org.apache.commons" % "commons-text" % "1.9", // for escaping strings in parser preprocessor
libraryDependencies += "commons-codec" % "commons-codec" % "1.15", // for obtaining the hex encoding of a string
libraryDependencies += "org.antlr" % "antlr4-runtime" % "4.12.0",
libraryDependencies += "org.scalaz" %% "scalaz-core" % "7.3.7", // used for EitherT

scalacOptions ++= Seq(
"-encoding", "UTF-8", // Enforce UTF-8, instead of relying on properly set locales
Expand Down
2 changes: 1 addition & 1 deletion src/main/antlr4/GoParser.g4
View file
Original file line number Diff line number Diff line change
Expand Up @@ -193,7 +193,7 @@ commCase: CASE (sendStmt | recvStmt) | DEFAULT;

recvStmt: (expressionList ASSIGN | identifierList DECLARE_ASSIGN)? recvExpr = expression;

forStmt: FOR (expression | forClause | rangeClause)? block;
forStmt: FOR (expression? | forClause | rangeClause?) block;

forClause:
initStmt = simpleStmt? eos expression? eos postStmt = simpleStmt?;
Expand Down
7 changes: 7 additions & 0 deletions src/main/java/viper/gobra/frontend/GobraParserBaseVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,13 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitSourceFile(GobraParser.SourceFileContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitPreamble(GobraParser.PreambleContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
Expand Down
7 changes: 7 additions & 0 deletions src/test/scala/viper/gobra/parsing/ParserUnitTests.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2755,4 +2755,11 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside {
) =>
}
}

test("Parser: should be able to parse an empty for clause") {
frontend.parseStmtOrFail("for { x := 42 }") should matchPattern {
case PForStmt(None, PBoolLit(true), None, PLoopSpec(Vector(), None), PBlock(Vector(PShortVarDecl(Vector(value), Vector(PIdnUnk(varname)), Vector(false)))))
if varname == "x" && value == PIntLit(42) =>
}
}
}
2 changes: 1 addition & 1 deletion viperserver
Submodule viperserver updated 4 files
+1 −1 carbon
+1 −1 silicon
+4 −0 src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala
+21 −3 src/main/scala/viper/server/frontends/lsp/FileManager.scala

0 comments on commit 948b641

Please sign in to comment.