id Summary Owner Type Priority Component Version 161 Automatic performance analysis zirkel task major Administration 1.0 181 Add derivative support to frontend zirkel task major front 1.0 239 store malloc statements in heap Stephen Siegel enhancement major multiple 1.0 160 "Prepare ""binary"" release" zirkel task critical Administration 1.0 122 add option to not stop after finding violation enhancement major verify 1.0 156 ClassCastException in TreeParser ywei defect major front 1.0 157 tuple support in symbolic universe incomplete ywei defect major symbolic 1.0 158 implement garbage collection Stephen Siegel task major semantics 1.0 159 use exact rational arithmetic? enhancement major multiple 1.0 162 Add unit test tree task major test 1.0 163 rationalize the command-line interface and class MiniMP ywei enhancement major User Interface 1.0 164 MiniMP language page needs to be fixed ywei task major Documentation 1.0 165 need cast from int to real operation in symbolic package ywei enhancement major symbolic 1.0 166 rename MiniMP-> TASS task major Administration 1.0 168 Examples need to be parametrized task major examples 1.0 169 front end and symbolic need to use BigRational, BigInteger ywei task major multiple 1.0 170 Add sizeof operator to front end ywei enhancement major front 1.0 171 Multiple improvements to binary release zirkel enhancement major Administration 175 Add sizeof expression to model package zirkel defect major model 1.0 176 longName() method in PointerType class may cause stack overflow Stephen Siegel defect major model 1.0 179 NullPointerException in DynamicFactory constructor Stephen Siegel defect major verify 1.0 180 When abstract functions are created, the continuity should be saved zirkel defect major front 1.0 184 Make library framework zirkel enhancement major None 1.0 186 null pointer exception from CVC3 prover ywei defect major prove 1.0 187 Array out of bound exception in AdderTest ywei defect major symbolic 1.0 188 Illegal argument exception in AdderTest Stephen Siegel defect major symbolic 1.0 189 Another illegal argument exception in AdderTest Stephen Siegel defect major symbolic 1.0 190 Add list of abstract functions to XML representation of model bperry enhancement major XML 1.0 192 string index error in parser ywei defect major front 1.0 194 nestedLoops: inconclusive result in v1.0 ywei defect major examples 1.0 195 missing diffusion_par.mmp defect major examples 1.0 197 linear time membership test in loop module defect major verify 1.0 198 PointerTest: record test has infinite recursion Stephen Siegel defect major dynamic 1.0 199 CVC3 prover does not handle MODULO ywei defect major prove 1.0 200 compilation error in model module zirkel defect major model 1.0 201 source release zirkel defect major Administration 1.0 203 Add support for record and array literal expressions to the front-end ywei enhancement major front 1.0 204 Allow array type variables to have initialization ywei defect major model 1.0 205 Extend evaluateLiteral in Evaluator to support records, arrays, and characters zirkel enhancement major semantics 1.0 206 Formal grammar for assertion and joint invariant language bperry task major XML 1.0 207 Add support for APPLY to CVC3TheoremProver task major prove 1.0 208 Separate pragma parsing out of language parser and put it into model builder bperry enhancement major front 1.0 209 Add support for APPLY operation in CVC3TheoremProver ywei defect major prove 1.0 212 move auto tests to anton zirkel task major test 1.0 214 Simplifier: x=y && y=2 does not simplify correctly on x Stephen Siegel enhancement major symbolic 1.0 215 Discrepency when simplifying using reals vs integers zirkel defect major dynamic 1.0 216 Simplifier: improper simplification when simplifying on an implication zirkel defect major symbolic 1.0 218 Failure in GradeCount loop test ywei defect major examples 1.0 220 No null constant value Stephen Siegel enhancement major symbolic 1.0 222 Infinite loop with pointer usage in .mmp file defect major examples 1.0 223 Parser error with pointer manipulation in .mmp file defect major examples 1.0 224 Free fails when used on a struct pointer. defect major examples 1.0 225 EvaluatedFunction not used zirkel defect major dynamic 1.0 226 heap canonicalization does not report leaks Stephen Siegel defect major state 1.0 227 Parser error when declaring a pointer and assigning it memory with malloc on same line. defect major examples 1.0 228 Error reporting issue when parsing .mmp file. defect major examples 1.0 229 Improve ExecutionException Stephen Siegel enhancement major multiple 1.0 230 null pointer exception in return statement ywei defect major front 1.0 231 add casts between pointer types zirkel enhancement major multiple 1.0 233 change grammar and examples to C notation enhancement major multiple 1.0 234 Parser Test fail on MPI_Init zirkel defect major front 1.0 236 source not getting set for malloc zirkel defect major front 1.0 237 reduce output from tests dfix task major test 1.0 240 free requires LHS expression in model builder zirkel defect major front 1.0 241 add assert to grammar ywei enhancement major front 1.0 242 problem with negative constants bperry defect major front 1.0 243 forall example needs accompanying JUnit test bperry task major test 1.0 244 shadow variables handled incorrectly zirkel defect major front 1.0 245 implement count correctly in MPI point-to-point ops Stephen Siegel defect major None 1.0 246 Foo function square no make sense zirkel defect major Administration 1.0 247 add guard expression to system function zirkel enhancement major front 1.0 248 add message to TASS assert zirkel enhancement major multiple 1.0 250 Make release 1.0 zirkel task major Administration 1.0 254 web page: bad example dfix defect major Publicity 1.0 155 Better error reporting from parser needed ywei enhancement minor Administration 1.0 191 source text not set correctly ywei defect minor front 1.0 193 source text for loop too big ywei defect minor front 1.0 196 source still too big ywei defect minor front 1.0 219 Cannot use -> on left hand of assignment in .mmp files Stephen Siegel defect minor examples 1.0 221 Cannot declare multiple variables on one line in .mmp zirkel enhancement minor front 1.0 238 source text for implicit return is empty bperry defect minor front 1.0 183 Verify derivative example using manual insertion of Taylor theorem zirkel enhancement major examples 1.0 202 installation from source task major Administration 1.0 211 don't check for deadlocked states when not necessary enhancement major verify 1.0 232 checkSat enhancement minor multiple 1.0