|
2945409 |
Examplar Incorrectly Substituted For in VCs |
Open
|
2010-02-03
|
hkeown
|
hwsmith
|
None
|
5
|
|
2945406 |
VCs corrupted for function operations |
Open
|
2010-02-03
|
hkeown
|
hwsmith
|
None
|
5
|
|
2907063 |
Conceptual Definitions Not Typed Correctly |
Open
|
2009-12-01
|
nobody
|
nobody
|
None
|
5
|
|
2905897 |
Undefined functions not reported in assertions |
Open
|
2009-11-30
|
hwsmith
|
hwsmith
|
None
|
5
|
|
2894370 |
VCs do not reflect clears |
Open
|
2009-11-09
|
hkeown
|
hwsmith
|
None
|
5
|
|
2891340 |
missing code? |
Open
|
2009-11-03
|
hkeown
|
eforney
|
None
|
5
|
|
2890841 |
Incorrect or Incomplete VCs |
Closed
|
2009-11-02
|
hkeown
|
hwsmith
|
Fixed
|
5
|
|
2883326 |
Error when a local function returns a record |
Open
|
2009-10-21
|
nobody
|
sitaraman
|
None
|
6
|
|
2883322 |
Analysis: Undeclared math def not caught |
Open
|
2009-10-21
|
nobody
|
sitaraman
|
None
|
5
|
|
2883275 |
Debugging info is printed out |
Open
|
2009-10-21
|
nobody
|
sitaraman
|
None
|
3
|
|
2881941 |
Math type resolution problems |
Open
|
2009-10-19
|
nobody
|
sitaraman
|
None
|
5
|
|
2881907 |
Math defn argument appears in code generation |
Closed
|
2009-10-19
|
sitaraman
|
sitaraman
|
Fixed
|
5
|
|
2880622 |
Precondition checking VC incorrect |
Open
|
2009-10-16
|
hkeown
|
nobody
|
None
|
5
|
|
2880535 |
Conc. variable initialization |
Closed
|
2009-10-16
|
sitaraman
|
sitaraman
|
Invalid
|
5
|
|
2831322 |
Disjuncts are not handled |
Open
|
2009-08-03
|
hwsmith
|
hwsmith
|
None
|
5
|
|
2831321 |
Verifier bombs with no Ensures |
Open
|
2009-08-03
|
hkeown
|
hwsmith
|
Fixed
|
5
|
|
2727220 |
Strings not supported |
Open
|
2009-04-02
|
nobody
|
sstrang
|
None
|
5
|
