search

viperproject / gobra

Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
https://gobra.ethz.ch
Other
112 stars 28 forks source link

Error reporting for imported packages containing errors #69

Closed viper-admin closed 4 years ago

viper-admin commented 4 years ago

Pull request :twisted_rightwards_arrows: created by @arquintl on 2020-06-26 13:18 Last updated on 2020-09-01 14:14 Original Bitbucket pull request id: 23

Participants:

  • bitbucket user Wytse Oortwijn (reviewer)
  • @arquintl
  • @Felalolf (reviewer) :heavy_check_mark:

Source: https://github.com/viperproject/gobra/commit/83f6195a8e78c14d4b43f401020beb9c2bb349a3 on branch import-error-reporting Destination: https://github.com/viperproject/gobra/commit/d1bb52792d91a5a5ce06ffb65cfd2d335caf58c7 on branch master Marge commit: https://github.com/viperproject/gobra/commit/cf1bb2c5d11050342f530477d9df3c2dab05dbfb

State: MERGED

A type error is shown at the import statement in the following cases:

There is only a differentiation between not finding any source files for the package and parse & type errors. To get the specific errors one has to compile/verify the erroneous package itself

Depends on https://github.com/viperproject/gobra/pull/67

‌

viper-admin commented 4 years ago

@arquintl commented on 2020-07-17 12:37

This PR is now ready to be reviewed

viper-admin commented 4 years ago

@Felalolf commented on 2020-08-11 12:09

Location: line 67 of src/main/scala/viper/gobra/frontend/info/Info.scala

Why can errors occur multiple times?

viper-admin commented 4 years ago

@Felalolf commented on 2020-08-11 12:30

Location: line 179 of src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala

What would happen, if you replace 

info <- Info.check(parsedProgram, context)(config)

with 

info <- Right(new TypeInfoImpl(new GoTree(parsedProgram), context)(config))

(i.e. just not call .errors on the TypeInfo Object)?

viper-admin commented 4 years ago

@Felalolf commented on 2020-08-11 12:40

Outdated location: line 198 of src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala

you are computing alternativeErr, regardless of whether it is actually required or not.

viper-admin commented 4 years ago

@Felalolf commented on 2020-08-11 12:41

I went over it once

viper-admin commented 4 years ago

@arquintl commented on 2020-08-31 09:52

Location: line 67 of src/main/scala/viper/gobra/frontend/info/Info.scala

Why can errors occur multiple times?

// consider this: each error in an imported package is converted to an error at the import node with
// message 'Package <pkg name> contains errors'. If the imported package contains 2 errors then only a single error
// should be reported at the import node instead of two.

I’ve added this to the souce file

viper-admin commented 4 years ago

@arquintl commented on 2020-08-31 10:02

Location: line 179 of src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala

What would happen, if you replace 

info <- Info.check(parsedProgram, context)(config)

with 

info <- Right(new TypeInfoImpl(new GoTree(parsedProgram), context)(config))

(i.e. just not call .errors on the TypeInfo Object)?

I get an violation for UnknownType in typeD in the desugarer when desugaring the imported package and the imported package does not type

viper-admin commented 4 years ago

@arquintl commented on 2020-08-31 10:04

Outdated location: line 198 of src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala

you are computing alternativeErr, regardless of whether it is actually required or not.

fixed

viper-admin commented 4 years ago

@Felalolf approved :heavy_check_mark: the pull request on 2020-09-01 14:07