Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / sosy-lab/sv-witnesses issues and pull requests

#63 - `flow_insensitive_invariant` YAML entry type

Pull Request - State: open - Opened by sim642 over 2 years ago

#62 - `location_invariant` YAML entry type as schema

Pull Request - State: open - Opened by sim642 over 2 years ago

#61 - Combined schema for YAML witnesses

Pull Request - State: open - Opened by sim642 over 2 years ago - 6 comments

#60 - YAML-based format: Rename `loop_invariant` entry?

Issue - State: open - Opened by michael-schwarz over 2 years ago - 3 comments

#59 - Introduce entry type 'location_invariant' for YAML-based witnesses.

Pull Request - State: open - Opened by SvenUmbricht over 2 years ago - 1 comment

#58 - Point to witness validation script in CPAchecker

Pull Request - State: closed - Opened by MartinSpiessl almost 3 years ago

#57 - Output linter version during execution

Pull Request - State: closed - Opened by SvenUmbricht almost 3 years ago - 8 comments

#56 - Show overview of witness after linting.

Pull Request - State: closed - Opened by SvenUmbricht about 3 years ago

#55 - Let WitnessLint output the type of the witness

Issue - State: closed - Opened by dbeyer about 3 years ago - 4 comments

#54 - Extend --excludeRecentChecks

Pull Request - State: closed - Opened by SvenUmbricht about 3 years ago - 3 comments

#53 - Improve version output of the witness linter

Issue - State: closed - Opened by MartinSpiessl about 3 years ago

#52 - Add option to not perform recently added checks

Pull Request - State: closed - Opened by SvenUmbricht about 3 years ago

#51 - WIP: Proper handling of thread information in witness linter

Pull Request - State: open - Opened by SvenUmbricht about 3 years ago - 1 comment

#50 - WIP: Simplify/Update validation instructions for CPAchecker

Pull Request - State: open - Opened by MartinSpiessl over 3 years ago

#49 - Linter crashes on seemingly valid witness

Issue - State: closed - Opened by danieldietsch over 3 years ago - 1 comment
Labels: bug

#48 - Linter rejects witness with tool-specific edge data element

Issue - State: closed - Opened by hernanponcedeleon over 3 years ago - 1 comment

#47 - Forbid use of local time in "creationtime" entries

Pull Request - State: closed - Opened by SvenUmbricht over 3 years ago

#46 - Migrate main branch name

Issue - State: closed - Opened by MartinSpiessl over 3 years ago

#44 - Invariant witnesses

Pull Request - State: closed - Opened by dbeyer over 3 years ago

#43 - Add SV-COMP-specific specfication check.

Pull Request - State: closed - Opened by dbeyer over 3 years ago

#42 - Clarify in the documentation if `programhash` is allowed to be SHA-1

Issue - State: closed - Opened by RyanGlScott over 3 years ago - 3 comments

#41 - Example witness files in the repo do not pass linter

Issue - State: open - Opened by RyanGlScott over 3 years ago - 2 comments

#40 - Witness linter rejects ISO 8601 times with decimal components

Issue - State: open - Opened by RyanGlScott over 3 years ago - 3 comments
Labels: enhancement

#39 - Create python package for linter

Pull Request - State: open - Opened by SvenUmbricht over 3 years ago - 5 comments

#38 - Violation witness clarification

Issue - State: open - Opened by hernanponcedeleon almost 4 years ago - 3 comments

#36 - WitnessLinter ignores threads when checking callstack validity.

Issue - State: open - Opened by kfriedberger about 4 years ago - 3 comments
Labels: bug, non-breaking change

#35 - Disable threadId check about repeated thread creation.

Pull Request - State: closed - Opened by kfriedberger about 4 years ago

#33 - WitnessLinter does not consider different paths in a witness when checking thread information

Issue - State: open - Opened by kfriedberger about 4 years ago - 2 comments
Labels: bug, non-breaking change, underspecification

#32 - Clarification of keys `cycle-head` and `invariant` is needed for termination witnesses

Issue - State: open - Opened by MartinSpiessl about 4 years ago - 2 comments
Labels: enhancement, help wanted, underspecification

#31 - Use default when checking for invariants on cycle heads

Pull Request - State: closed - Opened by maul-esel about 4 years ago - 7 comments

#30 - Specification fix: ensure that the initial thread can be referenced

Pull Request - State: open - Opened by tautschnig about 4 years ago - 1 comment

#29 - Disable ThreadId check as the spec needs to be clarified first

Pull Request - State: closed - Opened by tautschnig about 4 years ago - 1 comment

#28 - Create CI tests for the witness linter

Issue - State: open - Opened by MartinSpiessl about 4 years ago
Labels: enhancement

#27 - Create python package (pip?) for witness linter

Issue - State: open - Opened by MartinSpiessl about 4 years ago

#26 - Introduce annotation for format version

Pull Request - State: closed - Opened by MartinSpiessl about 4 years ago

#25 - Fix typo in control key specification

Pull Request - State: closed - Opened by MartinSpiessl about 4 years ago

#24 - Allow schema location attribute on graphml element

Pull Request - State: closed - Opened by maul-esel about 4 years ago - 1 comment

#23 - Add a way to specify witness format versions

Issue - State: closed - Opened by MartinSpiessl about 4 years ago

#22 - Reconsider the `architecture` description in the witness graphml files

Issue - State: open - Opened by MartinSpiessl about 4 years ago - 1 comment
Labels: enhancement, non-breaking change, blocked

#21 - Attributes on graphml element

Issue - State: closed - Opened by maul-esel about 4 years ago - 3 comments

#20 - Clarification needed for line number information of returnFromFunction

Issue - State: closed - Opened by shaobo-he about 4 years ago - 6 comments

#19 - Feature request: Python API

Issue - State: open - Opened by shaobo-he about 4 years ago - 2 comments
Labels: enhancement, help wanted

#18 - Make repository reuse compliant

Issue - State: open - Opened by MartinSpiessl over 4 years ago - 1 comment

#17 - Alternative Format for Correctness Witnesses

Issue - State: closed - Opened by MartinSpiessl over 4 years ago - 17 comments
Labels: enhancement

#16 - Add witnesses checker (linter)

Pull Request - State: closed - Opened by SvenUmbricht over 4 years ago - 23 comments

#14 - Example for a correctness witness contains forbidden data key `control`

Issue - State: open - Opened by MartinSpiessl over 4 years ago - 13 comments

#13 - Examples do not match documentation

Issue - State: closed - Opened by tautschnig almost 6 years ago - 1 comment

#12 - Missing semantics

Issue - State: closed - Opened by tautschnig almost 6 years ago - 2 comments

#11 - Please provide links to preprints of papers

Issue - State: closed - Opened by PhilippWendler about 6 years ago - 1 comment

#10 - Fix the script for witness validation service add ad it to repo directlyFixservice

Pull Request - State: closed - Opened by vlstill over 6 years ago - 1 comment

#9 - Example of a concurrency witness

Issue - State: closed - Opened by peterschrammel about 7 years ago - 2 comments

#8 - adding minimal example witness for a concurrent task.

Pull Request - State: closed - Opened by kfriedberger about 7 years ago - 2 comments

#7 - update section about termination witnesses for Ultimate Automizer

Pull Request - State: closed - Opened by danieldietsch about 7 years ago

#6 - added a block to termination witnesses

Pull Request - State: closed - Opened by Eiram about 7 years ago

#5 - initial text for concurrent witnesses.

Pull Request - State: closed - Opened by kfriedberger about 7 years ago

#4 - Command lines for witness validation are outdated

Issue - State: open - Opened by PhilippWendler over 7 years ago - 6 comments

#3 - CPAchecker command line for test harnesses is invalid

Issue - State: closed - Opened by PhilippWendler over 7 years ago - 1 comment

#2 - Output flag sensitive to trailing separator

Issue - State: closed - Opened by joshuata about 8 years ago - 4 comments

#1 - Documentation for test harnesses mentions test/programs/benchmarks

Issue - State: closed - Opened by PhilippWendler about 8 years ago - 1 comment