reorganize files

src/main/scala/viper/gobra/frontend/Desugar.scala

@@ -16,7 +16,7 @@ import viper.gobra.frontend.info.base.Type._
 import viper.gobra.frontend.info.base.{BuiltInMemberTag, Type, SymbolTable => st}
 import viper.gobra.frontend.info.implementation.resolution.MemberPath
 import viper.gobra.frontend.info.{ExternalTypeInfo, TypeInfo}
-import viper.gobra.reporting.Source.{AutoImplProofAnnotation, MainPreNotEstablished}
+import viper.gobra.reporting.Source.{AutoImplProofAnnotation, ImportPreNotEstablished, MainPreNotEstablished}
 import viper.gobra.reporting.{DesugaredMessage, Source}
 import viper.gobra.theory.Addressability
 import viper.gobra.translator.Names
@@ -3466,15 +3466,14 @@ object Desugar extends LazyLogging {
 
       // Check that all import preconditions of imported packages are implied by those packages'
       // friend clauses.
-      val currPkgUniqId = mainPkg.info.uniquePath
       val resourcesToPkg = initSpecs.getImportsFromMainPkg()
       resourcesToPkg.foreach{ case (pkg, resources) =>
         val src = meta(mainPkg, info)
-        val importObligationsOpt = checkPkgImportObligations(mainPkg, pkg, resources, initSpecs)(src)
+        val annotatedSrc = src.createAnnotatedInfo(ImportPreNotEstablished)
+        val importObligationsOpt = checkPkgImportObligations(mainPkg, pkg, resources, initSpecs)(annotatedSrc)
         importObligationsOpt.foreach(AdditionalMembers.addMember)
       }
 
-
       // if the main function is present, check its proof obligations
       val mainFuncObligations = generateMainFuncProofObligation(mainPkg, initSpecs)
       mainFuncObligations.foreach(AdditionalMembers.addMember)

src/test/resources/same_package/import-fail01-pkginvs/bar/bar.gobra → src/test/resources/same_package/import1/bar/bar.gobra

@@ -1,9 +1,12 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-initEnsures acc(&A) && acc(&B) && acc(&C)
 package bar
 
+// ##(-I ../)
+
+friendPkg "pkg" acc(&A) && acc(&B) && acc(&C)
+
 var A@ int = 1
 var B@ int = 2
 var C@ int = 3

src/test/resources/same_package/import-fail01-pkginvs/importer1.gobra → src/test/resources/same_package/import1/pkg/importer1.gobra

@@ -1,8 +1,9 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-package main
+package pkg
+
+// ##(-I ../)
 
-// ##(-I ./)
 importRequires acc(&bar.A) && acc(&bar.B)
 import "bar"

src/test/resources/same_package/import1/pkg/importer2.gobra

@@ -0,0 +1,9 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package pkg
+
+// ##(-I ../)
+
+importRequires acc(&bar.C)
+import "bar"

src/test/resources/same_package/import2/bar/bar.gobra

@@ -0,0 +1,12 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package bar
+
+// ##(-I ../)
+
+friendPkg "pkg" acc(&A) && acc(&B) && acc(&C)
+
+var A@ int = 1
+var B@ int = 2
+var C@ int = 3

src/test/resources/same_package/import2/pkg/importer1.gobra

@@ -0,0 +1,9 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package pkg
+
+// ##(-I ../)
+
+importRequires acc(&bar.A) && acc(&bar.B)
+import "bar"

src/test/resources/same_package/import-fail01-pkginvs/importer2.gobra → src/test/resources/same_package/import2/pkg/importer2.gobra

@@ -1,9 +1,10 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-package main
+package pkg
+
+// ##(-I ../)
 
-// ##(-I ./)
 //:: ExpectedOutput(import_pre_error)
 importRequires acc(&bar.B) && acc(&bar.C)
 import "bar"

src/test/resources/same_package/pkg_init/scion/scion.go

@@ -19,7 +19,6 @@ import (
 	// @ importRequires path.PkgInv()
 	// @ importRequires path.RegisteredTypes().DoesNotContain(1) &&
 	// @ 	path.RegisteredTypes().DoesNotContain(2)
-	// importRequires false // TODO: check and then drop
 	// @ "scion/path"
 	"scion/path/onehop"
 	"scion/path/scion"
@@ -33,5 +32,4 @@ import (
 func init() {
 	scion.RegisterPath()
 	onehop.RegisterPath()
-	//  assert false
 }