Summary: gathering of known bugs, shortcomings, nuisances, etc.

Spec#

This area deals with the Spec# compiler proper.

True Bugs

Something that truly does not behave as documented (or as inferred from documentation and goals of Spec#), and that will be fixed in a "future release"

Arguable Bugs

Something that deviates from "expected" behaviour, but for which there is not yet a consensus that is is a bug and has to be fixed in a "future release"

* WarnIfContractAssemblyElementNotApplicableBug -- Issue a warning when compiling a shadow assembly and some element of the shadow assembly has no counterpart in the assembly being shadowed. More generally, issue a warning if something has no effect, which is usually a mistake.

Nuisances

Things that deviate from "expected" behaviour, but have been determined to not be a bug, and for which there is no plan to attempt to conform with "expected" behaviour

Spec# Program Verifier

True Bugs

* ConstructedTypeMethodContractsNotResolvedBug -- A call of a method of a constructed type causes the Spec# Program Verifier to crash if the method has a contract and the contract contains things that need to be resolved, such as qualified identifiers.

Arguable Bugs

Nuisances

IDE

True Bugs (or incomplete features)

* FooNotFooBug -- false complaint about type mismatch

* SourceControlBug -- Source Control integration (such as pending checkins) works for Spec# projec files, but not Spec# source files

* DifferentResultsBug -- sometimes consecutive solution rebuilds yield different errors/warnings.

Arguable Bugs (or potential new features)

Nuisances

Specifications

This area deals with specifications provided by the Spec# team for non-Spec# APIs, such as standard C#/.NET assemblies like System.String, System.Collections, ...