Skip to content

Conversation

@emarzion
Copy link
Contributor

@emarzion emarzion commented Jan 28, 2021

Fixes #2360, #2356, #2355

  • adds new module Kore.Log.WarnBoundedModelChecker
  • adds location info + klabel info to WarnFunctionWithoutEvaluators
  • adds SomeClaim field to WarnStuckClaimState
  • adds claim field to CheckResult
  • moves stuck claim state warnings from Kore.Reachability.Claim to Kore.Reachability.Prove
Review checklist

The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.

  • Summary. Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history.
  • Documentation. Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing.
  • Tests. Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests.
  • Clean up. The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes!

@emarzion emarzion changed the title adding log entry for bounded model checker Adding missing location information to various warnings Feb 2, 2021
@ttuegel ttuegel marked this pull request as ready for review February 2, 2021 15:05
emarzion and others added 10 commits February 3, 2021 09:30
Co-authored-by: Thomas Tuegel <thomas.tuegel@runtimeverification.com>
Co-authored-by: Thomas Tuegel <thomas.tuegel@runtimeverification.com>
Co-authored-by: Andrei Burdușa <53746396+andreiburdusa@users.noreply.github.com>
Co-authored-by: Andrei Burdușa <53746396+andreiburdusa@users.noreply.github.com>
emarzion and others added 6 commits February 4, 2021 23:11
@emarzion emarzion merged commit feb64cd into master Feb 5, 2021
@emarzion emarzion deleted the new-log-entries branch February 5, 2021 06:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Add location information to bounded model checker warnings

4 participants