Whiley/Whiley2Boogie issues and pull requests

#163 - Add tests submodule

Issue - State: open - Opened by DavePearce over 2 years ago

#162 - Check Property Preconditions

Issue - State: open - Opened by DavePearce over 2 years ago - 1 comment
Labels: enhancement

#161 - Problem with Nested Quantifier

Issue - State: closed - Opened by DavePearce over 2 years ago - 1 comment
Labels: bug

#160 - Duplicate Variables

Issue - State: closed - Opened by DavePearce over 2 years ago
Labels: bug

#159 - Update Property Translation

Issue - State: closed - Opened by DavePearce over 2 years ago
Labels: enhancement

#158 - Verification and Lambda's

Issue - State: open - Opened by DavePearce over 5 years ago

#157 - Add more Negative Range Tests

Issue - State: closed - Opened by DavePearce over 2 years ago

#156 - Static Type Invariants

Issue - State: closed - Opened by DavePearce over 2 years ago
Labels: bug

#155 - Support old() for static variables

Issue - State: closed - Opened by DavePearce over 2 years ago - 1 comment

#154 - Exponetiation

Issue - State: closed - Opened by DavePearce over 2 years ago - 4 comments

#153 - Boogie Backend Redesign

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

#152 - Definedness of Properties

Issue - State: closed - Opened by DavePearce over 2 years ago - 2 comments
Labels: bug

#151 - Implement ArrayUpdate and RecordUpdate operators

Issue - State: closed - Opened by DavePearce over 2 years ago
Labels: enhancement

#150 - Look at Move Prover?

Issue - State: closed - Opened by DavePearce almost 3 years ago
Labels: enhancement

#149 - Negative Range Error

Issue - State: closed - Opened by DavePearce almost 3 years ago

#148 - Missing Invariant Checks for Casts

Issue - State: open - Opened by DavePearce almost 3 years ago - 3 comments
Labels: bug

#147 - Negative Ranges in Quantifiers

Issue - State: closed - Opened by DavePearce almost 3 years ago
Labels: bug

#146 - Problem with Templates and (In)equality

Issue - State: closed - Opened by DavePearce almost 3 years ago - 1 comment

#145 - IllegalArgumentException

Issue - State: closed - Opened by DavePearce almost 3 years ago - 7 comments
Labels: bug

#144 - Counterexample Generation

Issue - State: open - Opened by DavePearce almost 3 years ago

#143 - Enable choice over verifying external code

Issue - State: open - Opened by DavePearce almost 3 years ago
Labels: enhancement

#142 - Typed Version of Heap

Issue - State: closed - Opened by DavePearce almost 3 years ago

#141 - Support Alternative Provers

Issue - State: closed - Opened by DavePearce almost 3 years ago - 1 comment
Labels: enhancement

#140 - Support Linking

Issue - State: closed - Opened by DavePearce almost 3 years ago
Labels: enhancement

#139 - Update for WhileyBuildTool

Issue - State: closed - Opened by DavePearce almost 3 years ago
Labels: enhancement

#138 - Assigning Static Fields

Issue - State: closed - Opened by DavePearce about 3 years ago - 1 comment

#137 - Unexpected Loop Invariant Failure

Issue - State: closed - Opened by DavePearce about 3 years ago - 1 comment
Labels: bug

#136 - Representing MultiSets

Issue - State: open - Opened by DavePearce about 3 years ago - 2 comments
Labels: enhancement

#135 - Support Boogie Options

Issue - State: closed - Opened by DavePearce about 3 years ago - 1 comment
Labels: enhancement

#134 - Method Calls in Loops

Issue - State: open - Opened by DavePearce about 3 years ago - 5 comments
Labels: bug

#133 - Bug with Expanding For Loop Invariants??

Issue - State: closed - Opened by DavePearce about 3 years ago - 3 comments
Labels: bug

#132 - Problem with array::append

Issue - State: open - Opened by DavePearce about 3 years ago
Labels: bug

#131 - Finding Triggers

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

#130 - NullPointerException

Issue - State: closed - Opened by DavePearce over 3 years ago - 2 comments
Labels: bug

#129 - Trigger Discovery

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

#128 - Recursive Variants

Issue - State: open - Opened by DavePearce over 3 years ago
Labels: bug

#127 - Support Loop Invariants and Old() Syntax

Issue - State: open - Opened by DavePearce over 3 years ago - 3 comments
Labels: bug

#126 - Support Old Syntax

Issue - State: closed - Opened by DavePearce over 3 years ago - 3 comments
Labels: enhancement

#125 - Update to WyC 0.9.7

Issue - State: closed - Opened by DavePearce over 3 years ago
Labels: enhancement

#124 - Support Unsafe Modifier

Issue - State: closed - Opened by DavePearce over 3 years ago
Labels: enhancement

#123 - Framing Indirect Method Invocation

Issue - State: open - Opened by DavePearce over 3 years ago
Labels: bug

#122 - Type Checking Error

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

#121 - Problem with Function Calls in Loop Conditions

Issue - State: closed - Opened by DavePearce over 3 years ago
Labels: bug

#120 - Postcondition Axiom (again)

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

#119 - Multi-Assignment and Disjointness

Issue - State: open - Opened by DavePearce over 3 years ago - 2 comments
Labels: bug

#118 - Bug with (Multi-)Dimensional Quantifiers ?

Issue - State: closed - Opened by DavePearce over 3 years ago - 2 comments
Labels: bug

#117 - Typechecker loses precision?

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

#116 - Bug with Vector Sum?

Issue - State: closed - Opened by DavePearce over 3 years ago
Labels: bug

#115 - Problem with Reference Assignment

Issue - State: open - Opened by DavePearce almost 4 years ago - 5 comments
Labels: bug

#114 - Generated Procedures should used Pre and Post

Issue - State: closed - Opened by DavePearce almost 4 years ago
Labels: enhancement

#113 - Temporarily-broken record invariants

Issue - State: closed - Opened by utting almost 4 years ago - 2 comments

#112 - HEAP missing in constant definitions

Issue - State: open - Opened by utting almost 4 years ago

#111 - Consistency of (Array) Axioms

Issue - State: closed - Opened by DavePearce almost 4 years ago - 6 comments
Labels: bug, enhancement

#110 - Tidying up Array#is

Issue - State: open - Opened by DavePearce almost 4 years ago
Labels: enhancement

#109 - Boogie Sequences

Issue - State: closed - Opened by DavePearce almost 4 years ago

#108 - Trigger Syntax

Issue - State: closed - Opened by DavePearce almost 4 years ago

#107 - Boogie Tuple Assignments

Issue - State: closed - Opened by DavePearce almost 4 years ago

#106 - Translation of Type Variables

Issue - State: open - Opened by DavePearce almost 4 years ago
Labels: bug

#105 - Guards for Array Axioms

Issue - State: closed - Opened by DavePearce almost 4 years ago - 5 comments
Labels: bug

#104 - Boogie Assertion Messages

Issue - State: closed - Opened by DavePearce almost 4 years ago
Labels: enhancement

#103 - Problem with Lambda Translation

Issue - State: open - Opened by DavePearce almost 4 years ago
Labels: bug

#102 - Array Update Axiom Problem

Issue - State: closed - Opened by DavePearce almost 4 years ago - 1 comment
Labels: bug

#101 - Array Model in Boogie

Issue - State: closed - Opened by DavePearce almost 4 years ago
Labels: enhancement

#100 - Problem with Reference Type in Loop

Issue - State: closed - Opened by DavePearce almost 4 years ago - 2 comments
Labels: bug

#99 - (Non-Atomic) Multiple Assignments

Issue - State: closed - Opened by DavePearce almost 4 years ago
Labels: bug

#98 - Problem with Large Static Initialiser

Issue - State: closed - Opened by DavePearce almost 4 years ago
Labels: bug

#97 - Reference Type Invariant not Preserved in Loop

Issue - State: closed - Opened by DavePearce almost 4 years ago - 1 comment
Labels: bug

#96 - Problem with nested Lambda

Issue - State: closed - Opened by DavePearce almost 4 years ago - 1 comment
Labels: bug

#95 - Boogie Errors being silently dropped

Issue - State: closed - Opened by DavePearce almost 4 years ago - 1 comment
Labels: bug

#94 - Problematic Non-Linear Kernels

Issue - State: closed - Opened by DavePearce almost 4 years ago - 2 comments

#93 - Flag to Disable Name Mangling

Issue - State: closed - Opened by DavePearce almost 4 years ago - 2 comments
Labels: enhancement

#92 - Source Line Infor for Loop Invariants

Issue - State: closed - Opened by DavePearce almost 4 years ago
Labels: bug

#91 - Instant timeouts (Linux-specific?)

Issue - State: closed - Opened by l-kent almost 4 years ago - 18 comments

#90 - Link Unresolved

Issue - State: closed - Opened by DavePearce almost 4 years ago - 2 comments
Labels: bug

#89 - Problem with Templates and References?

Issue - State: open - Opened by DavePearce almost 4 years ago
Labels: bug

#88 - Problem with std::collections::hash_map

Issue - State: closed - Opened by DavePearce almost 4 years ago - 1 comment
Labels: bug

#87 - Unchecked Type Invariant

Issue - State: closed - Opened by DavePearce almost 4 years ago - 2 comments
Labels: bug

#86 - Unchecked Loop Invariant

Issue - State: closed - Opened by DavePearce almost 4 years ago - 3 comments
Labels: bug

#85 - Unchecked Cast

Issue - State: closed - Opened by DavePearce almost 4 years ago - 1 comment
Labels: bug

#84 - Unchecked Precondition

Issue - State: closed - Opened by DavePearce almost 4 years ago - 4 comments
Labels: bug

#83 - Problem with Meta Types

Issue - State: closed - Opened by DavePearce almost 4 years ago
Labels: bug

#82 - WellDefinedness of Loop Conditions

Issue - State: closed - Opened by DavePearce almost 4 years ago - 2 comments

#81 - Problem with Type Tests and Loop Invariants

Issue - State: open - Opened by DavePearce almost 4 years ago
Labels: enhancement

#78 - Well-Definedness in Specification Elements

Issue - State: closed - Opened by DavePearce almost 4 years ago - 6 comments
Labels: enhancement

#77 - Support "free" expression

Issue - State: closed - Opened by DavePearce almost 4 years ago
Labels: enhancement

#76 - Implement Methods as for Functions

Issue - State: closed - Opened by DavePearce almost 4 years ago - 6 comments

#74 - Refactoring for Side-Effects and Well-Definedness

Issue - State: closed - Opened by DavePearce almost 4 years ago - 4 comments

#72 - Record of Limitations

Issue - State: open - Opened by DavePearce about 4 years ago - 1 comment

#70 - Loop-Used Variables and References

Issue - State: closed - Opened by DavePearce about 4 years ago
Labels: bug

#67 - Non-Termination Problems

Issue - State: closed - Opened by DavePearce about 4 years ago - 1 comment
Labels: bug

#66 - Lambda Type Invariant with Templates

Issue - State: closed - Opened by DavePearce about 4 years ago
Labels: bug

#64 - Refactor Function Lambda's

Issue - State: closed - Opened by DavePearce about 4 years ago
Labels: enhancement

#61 - Problem with Cyclic Reference Type Invariants

Issue - State: open - Opened by DavePearce about 4 years ago - 2 comments

#60 - Preserving loop invariant HEAP locations

Issue - State: open - Opened by DavePearce about 4 years ago - 23 comments
Labels: bug

#59 - Problem with Lambda Unions

Issue - State: closed - Opened by DavePearce about 4 years ago - 1 comment

#56 - Problem with Dereference in Postcondition

Issue - State: closed - Opened by DavePearce about 4 years ago - 1 comment
Labels: bug

#39 - WyBench Status

Issue - State: closed - Opened by DavePearce about 4 years ago - 1 comment

#37 - Error Reporting

Issue - State: closed - Opened by DavePearce about 4 years ago
Labels: enhancement

#26 - Problem with Existential?

Issue - State: closed - Opened by DavePearce about 4 years ago - 3 comments
Labels: bug

#21 - Unsoundness of Functions and Constants.

Issue - State: closed - Opened by DavePearce about 4 years ago - 20 comments

GitHub / Whiley/Whiley2Boogie issues and pull requests