id Summary Owner Type Priority Milestone Component 125 "add line number for ""implicit return""" ywei enhancement trivial front 144 Improvements to source text ywei enhancement trivial front 4 ugly output in verbose mode ywei defect minor front 5 command line interface corrections ywei defect minor front 6 text associated to branch statements ywei enhancement minor front 7 white space in text ywei enhancement minor front 10 command line interface additions ywei enhancement minor front 15 prover debugging output should print result ywei enhancement minor symbolic 21 improvements to user interface ywei enhancement minor User Interface 23 printing of symbolic expressions needs improvement ywei enhancement minor symbolic 25 SyntaxException when verifying matmat-seq.mmp zirkel defect minor examples 28 improvements to model printing with source ywei enhancement minor model 30 improve model names ywei enhancement minor User Interface 31 "deprecated ""\O"" notation occurs in diffusion example" zirkel defect minor examples 34 Add for loop support to front end ywei enhancement minor front 40 change name of Minimp to MiniMP ywei task minor Administration 41 change the JUnit test zirkel defect minor test 51 add front end support for ++ and -- ywei enhancement minor front 55 enhance JUnit tests zirkel enhancement minor Administration 67 text associated to expressions has extra token ywei defect minor front 85 Integers cannot be set to negative literal ywei defect minor front 101 create BooleanValueIF Stephen Siegel enhancement minor value 105 Add support for new statements: pushassumption, popassumption enhancement minor multiple 106 Simplify print in model package enhancement minor model 124 improve performance of validity checking and other symbolic operations Stephen Siegel enhancement minor value 127 Improve symbolic variable names ywei enhancement minor symbolic 132 Need to shut down the dynamic factory when it is not in use Stephen Siegel defect minor value 138 source not set for sub-expressions of array subscript expressions ywei defect minor front 155 Better error reporting from parser needed ywei enhancement minor Release 1.0 Administration 172 Add check for the -inputX=N options Stephen Siegel enhancement minor model 178 Number of bound variables in a symbolic quantifier expression Stephen Siegel enhancement minor symbolic 191 source text not set correctly ywei defect minor Release 1.0 front 193 source text for loop too big ywei defect minor Release 1.0 front 196 source still too big ywei defect minor Release 1.0 front 219 Cannot use -> on left hand of assignment in .mmp files Stephen Siegel defect minor Release 1.0 examples 221 Cannot declare multiple variables on one line in .mmp zirkel enhancement minor Release 1.0 front 238 source text for implicit return is empty bperry defect minor Release 1.0 front 262 Make .externalToolBuilders/Ant_Builder.launch generic task minor Administration 273 Clean up front end names task minor front 298 "change method names in ast package involving ""name""" zirkel enhancement minor 1.1 ast 303 make invocation of clang parser portable defect minor 1.1 User Interface 305 Remove incorrect assertions stachnik defect minor ast 310 AST Parser: Print filename when reporting error stachnik enhancement minor 1.1 ast 311 Add print method to AbstractSyntaxTreeIF stachnik enhancement minor 1.1 ast 312 remove extraneous printing of AST stachnik defect minor 1.1 ast 1 null corresponding variable: tile example ywei defect major verify 2 null pointer exception in Evaluator Stephen Siegel defect major semantics 3 Execution exception in InnerPredicate Stephen Siegel defect major verify 8 symbolic expressions not being transformed into canonical form ywei enhancement major symbolic 9 multiple bugs in Urgent Stephen Siegel defect major verify 11 improve handling of counterexamples Stephen Siegel enhancement major search 12 Execution exception in Evaluator ywei defect major front 13 erratic behavior in symbolic package ywei defect major symbolic 14 flaw in simplify routine? ywei defect major symbolic 16 symbolic exception: arrayloop_2 ywei defect major symbolic 17 implement verify.loop ywei task major verify 18 examples zirkel task major examples 19 JUnit test cases zirkel task major examples 20 illegal reading of output variable zirkel defect major examples 22 automatic email zirkel task major Administration 26 Error in front-end on factorial example ywei defect major front 27 send-recv deadlock zirkel defect major examples 29 matrix multiplication tiling is incorrect zirkel defect major examples 32 casting between ints and reals ywei enhancement major symbolic 33 illegal use of output variable in matmat zirkel defect major examples 35 if-then-else ywei enhancement major multiple 36 Flag to control simplify ywei defect major multiple 37 Command line option to specify buffer bound ywei enhancement major front 39 format of examples zirkel defect major examples 42 CVC3 prover problems ywei defect major symbolic 43 matmat: send stmt parse exception ywei defect major front 44 Add for loop functionality to model zirkel enhancement major model 45 add support for initial values of scalar variables to model Stephen Siegel enhancement major model 46 add front end support for if-then-else ywei enhancement major front 47 add record types to model Stephen Siegel enhancement major model 48 add pointer types, values to model Stephen Siegel enhancement major model 50 add front end support for initialization expressions ywei enhancement major front 52 matrixMultiplication compare returns false ywei, zirkel defect major examples 53 Add <= operator to model Stephen Siegel defect major model 54 translate <= as lessThanOrEquals ywei enhancement major front 56 mean: null pointer exception ywei defect major front 57 nestedLoops: RuntimeException: Undefined value found. ywei defect major symbolic 58 simpleMP: Null pointer exception from parse ywei defect major front 59 skewFactor: Null pointer exception ywei defect major front 60 ArrayStoreException in simpleMP Stephen Siegel defect major state 61 null pointer exception in simpleMPSpec defect major front 62 infinite loop when verifying simpleMPSpec Stephen Siegel defect major search 63 errors in matmat-par_2_2_2.mmp zirkel defect major examples 64 error due to integer division in mean example defect major examples 65 JUnit test problem with SimpleMP zirkel defect major test 66 error in simpleMPImpl zirkel defect major examples 68 -loop option ywei enhancement major front 69 skewFactor: EmptyStackException ywei defect major front 70 Add abstract functions to frontend ywei enhancement major front 71 laplace example: inputs zirkel enhancement major examples 72 Make posters for accuracy verification and comparative symbolic execution ywei, zirkel task major Publicity 73 add Robert Deaton to Trac list zirkel task major Administration 74 Bus error using -simplify ywei defect major symbolic 75 Problems with tass verify, ArrayIndexOutOfBounds Exception Stephen Siegel defect major semantics 76 OSError: [Errno 13] Permission denied: '/vsl/trac/minimp/attachments/ticket' zirkel defect major Administration 77 unreachable location in matmat example defect major multiple 78 Class cast exception in matmat-par_2_2_2.mmp Stephen Siegel defect major semantics 79 for loop problem defect major front 80 simplify fails on dividing by plus expressions ywei defect major symbolic 81 add support for type ids Stephen Siegel enhancement major model 82 add record types and tuple types to symbolic package ywei enhancement major symbolic 83 Bug in checking equivalence of array outputs ywei defect major symbolic 84 Multiple additions to front end ywei enhancement major front 86 The target location is not being set for a select statement ywei defect major front 87 send report of API problems to cvc3 ywei task major Administration 89 send email to cvc3-users on non-linear accuracy example zirkel task major Administration 90 NullPointerException when using potential deadlock Stephen Siegel defect major verify 91 Add new directory in the branches for modelExtractor ywei task major Administration 92 add methods in symbolic universe to support unbound arrays ywei enhancement major symbolic 93 Add allocate and deallocate in the front end ywei enhancement major front 94 Update svn server Stephen Siegel task major Administration 95 improvements to symbolic package ywei enhancement major symbolic 96 parser should quit when syntax error encountered ywei defect major front 97 wrong function printed ywei defect major front 98 usage information incorrect ywei defect major User Interface 99 formal parameters have null source ywei defect major front 100 symbolic array dimensions are inverted ywei defect major symbolic 102 add concrete versions of primitive and array values Stephen Siegel enhancement major value 103 problem with build ywei defect major Administration 104 cast error in symbolic package defect major symbolic 107 Add symbolic function type enhancement major symbolic 108 array problem in symbolic ywei defect major symbolic 109 unknown expression type ywei defect major Administration 110 array compare problem in symbolic? ywei defect major Administration 111 matmat compare: outputs not equivalent? ywei defect major Administration 112 Parse error when declaring and assigning on the same line ywei defect major front 113 different behavior when using simplify ywei defect major multiple 114 TileTests fail Stephen Siegel defect major semantics 115 Laplace test errors zirkel defect major front 116 MatrixMultiplicationTests: compare failures defect major test 117 Problems with tests and use of static data ywei defect major test 118 Weird failure in MatrixMultiplication test defect major test 119 Errors in diffusion tests zirkel defect major test 120 rejected initialization expression x+y ywei defect major front 121 mean tests fail ywei defect major multiple 122 add option to not stop after finding violation enhancement major Release 1.0 verify 123 improve performance of hash and equality functions enhancement major multiple 126 sum tests fail ywei defect major test 128 Assume implementation error defect major semantics 129 simplify compare problem in matmat ywei defect major test 130 simpleArrayTest failure ywei defect major Administration 131 Extra assumptions in implementation not used Stephen Siegel defect major semantics 133 null pointer exception in model builder ywei defect major front 134 arithmetic parsing error ywei defect major front 135 syntax error in diffusion1_par.mmp zirkel defect major examples 136 Pointer type not parsed in formal parameter list ywei defect major front 137 pointer addition not in grammar ywei defect major front 139 running simpleRecordTest causes freeze defect major Administration 140 Pointer decl/initialization expression leads to NullPointerException in TreeParser ywei defect major front 141 simplify error in diffusion1 defect major Administration 142 Class cast exception in diffusion1 ywei defect major symbolic 143 source not set for allocate statements ywei defect major front 145 Add simplify method to SymUniverseIF ywei enhancement major symbolic 146 add to front-end: e[i] ywei enhancement major front 147 write outline for CAV tool paper zirkel task major Publicity 148 ClassCastException in dynamic package ywei defect major front 149 Tech report task major Publicity 150 Create web site task major Administration 151 Fib example gets wrong answer ywei defect major verify 152 front end does not parse certain type expressions ywei defect major front 153 implement XML representation of model bperry task major front 156 ClassCastException in TreeParser ywei defect major Release 1.0 front 157 tuple support in symbolic universe incomplete ywei defect major Release 1.0 symbolic 158 implement garbage collection Stephen Siegel task major Release 1.0 semantics 159 use exact rational arithmetic? enhancement major Release 1.0 multiple 162 Add unit test tree task major Release 1.0 test 163 rationalize the command-line interface and class MiniMP ywei enhancement major Release 1.0 User Interface 164 MiniMP language page needs to be fixed ywei task major Release 1.0 Documentation 165 need cast from int to real operation in symbolic package ywei enhancement major Release 1.0 symbolic 166 rename MiniMP-> TASS task major Release 1.0 Administration 168 Examples need to be parametrized task major Release 1.0 examples 169 front end and symbolic need to use BigRational, BigInteger ywei task major Release 1.0 multiple 170 Add sizeof operator to front end ywei enhancement major Release 1.0 front 171 Multiple improvements to binary release zirkel enhancement major Release 1.0 Administration 173 Add char type to model and value layer zirkel enhancement major multiple 174 Print intermediate report during execution Stephen Siegel enhancement major User Interface 175 Add sizeof expression to model package zirkel defect major Release 1.0 model 176 longName() method in PointerType class may cause stack overflow Stephen Siegel defect major Release 1.0 model 177 Add record literal expression in model package zirkel enhancement major model 179 NullPointerException in DynamicFactory constructor Stephen Siegel defect major Release 1.0 verify 180 When abstract functions are created, the continuity should be saved zirkel defect major Release 1.0 front 182 add evaluateEvaluatedFunction method to Executor zirkel enhancement major semantics 184 Make library framework zirkel enhancement major Release 1.0 None 185 Verification Suite zirkel task major Administration 186 null pointer exception from CVC3 prover ywei defect major Release 1.0 prove 187 Array out of bound exception in AdderTest ywei defect major Release 1.0 symbolic 188 Illegal argument exception in AdderTest Stephen Siegel defect major Release 1.0 symbolic 189 Another illegal argument exception in AdderTest Stephen Siegel defect major Release 1.0 symbolic 190 Add list of abstract functions to XML representation of model bperry enhancement major Release 1.0 XML 192 string index error in parser ywei defect major Release 1.0 front 194 nestedLoops: inconclusive result in v1.0 ywei defect major Release 1.0 examples 195 missing diffusion_par.mmp defect major Release 1.0 examples 197 linear time membership test in loop module defect major Release 1.0 verify 198 PointerTest: record test has infinite recursion Stephen Siegel defect major Release 1.0 dynamic 199 CVC3 prover does not handle MODULO ywei defect major Release 1.0 prove 200 compilation error in model module zirkel defect major Release 1.0 model 201 source release zirkel defect major Release 1.0 Administration 203 Add support for record and array literal expressions to the front-end ywei enhancement major Release 1.0 front 204 Allow array type variables to have initialization ywei defect major Release 1.0 model 205 Extend evaluateLiteral in Evaluator to support records, arrays, and characters zirkel enhancement major Release 1.0 semantics 206 Formal grammar for assertion and joint invariant language bperry task major Release 1.0 XML 207 Add support for APPLY to CVC3TheoremProver task major Release 1.0 prove 208 Separate pragma parsing out of language parser and put it into model builder bperry enhancement major Release 1.0 front 209 Add support for APPLY operation in CVC3TheoremProver ywei defect major Release 1.0 prove 210 Try to build solaris version of CVC3, etc. zirkel task major None 212 move auto tests to anton zirkel task major Release 1.0 test 213 Add array and record literals to frontend ywei defect major front 214 Simplifier: x=y && y=2 does not simplify correctly on x Stephen Siegel enhancement major Release 1.0 symbolic 215 Discrepency when simplifying using reals vs integers zirkel defect major Release 1.0 dynamic 216 Simplifier: improper simplification when simplifying on an implication zirkel defect major Release 1.0 symbolic 217 Add constants to model zirkel enhancement major model 218 Failure in GradeCount loop test ywei defect major Release 1.0 examples 220 No null constant value Stephen Siegel enhancement major Release 1.0 symbolic 222 Infinite loop with pointer usage in .mmp file defect major Release 1.0 examples 223 Parser error with pointer manipulation in .mmp file defect major Release 1.0 examples 224 Free fails when used on a struct pointer. defect major Release 1.0 examples 225 EvaluatedFunction not used zirkel defect major Release 1.0 dynamic 226 heap canonicalization does not report leaks Stephen Siegel defect major Release 1.0 state 227 Parser error when declaring a pointer and assigning it memory with malloc on same line. defect major Release 1.0 examples 228 Error reporting issue when parsing .mmp file. defect major Release 1.0 examples 229 Improve ExecutionException Stephen Siegel enhancement major Release 1.0 multiple 230 null pointer exception in return statement ywei defect major Release 1.0 front 231 add casts between pointer types zirkel enhancement major Release 1.0 multiple 233 change grammar and examples to C notation enhancement major Release 1.0 multiple 234 Parser Test fail on MPI_Init zirkel defect major Release 1.0 front 235 variadic formals Stephen Siegel enhancement major 1.1 multiple 236 source not getting set for malloc zirkel defect major Release 1.0 front 237 reduce output from tests dfix task major Release 1.0 test 240 free requires LHS expression in model builder zirkel defect major Release 1.0 front 241 add assert to grammar ywei enhancement major Release 1.0 front 242 problem with negative constants bperry defect major Release 1.0 front 243 forall example needs accompanying JUnit test bperry task major Release 1.0 test 244 shadow variables handled incorrectly zirkel defect major Release 1.0 front 245 implement count correctly in MPI point-to-point ops Stephen Siegel defect major Release 1.0 None 246 Foo function square no make sense zirkel defect major Release 1.0 Administration 247 add guard expression to system function zirkel enhancement major Release 1.0 front 248 add message to TASS assert zirkel enhancement major Release 1.0 multiple 249 Change signature of main to be consistent with C Stephen Siegel task major 1.1 examples 250 Make release 1.0 zirkel task major Release 1.0 Administration 251 initializing null pointer variable zirkel defect major 1.1 front 252 expand grammar for #define constants zirkel enhancement major 1.1 front 253 Improve syntax exception reporting bperry defect major 1.1 front 254 web page: bad example dfix defect major Release 1.0 Publicity 255 lib path wrong zirkel defect major 1.0.1 lib 256 Fix UI printout of revision number Stephen Siegel defect major 1.1 Administration 257 get rid of all compiler warnings zirkel defect major 1.0.1 multiple 258 TASS latest release contains tilde file zirkel defect major 1.1 Administration 259 javadoc not being executed zirkel defect major Administration 260 parser test failures zirkel defect major 1.1 front 261 Add support for #define input variables zirkel enhancement major 1.1 front 263 False guards are not getting reported as a deadlock Stephen Siegel defect major verify 264 null pointer exception in TreeParser using collective assert zirkel defect major 1.1 front 265 ModelBuilder runtime exception zirkel defect major 1.1 front 266 diffusion/ghost: no main function? defect major 1.1 front 267 collective assertion not getting added to model in unbalanced1.c zirkel defect major 1.1 front 268 no extra locations for collective assertions... zirkel defect major 1.1 front 270 implement local variable refs in collectives assertions zirkel task major 1.1 front 271 Cobertura report generation down defect major 1.1 scripts 272 Regular invariant not being added correctly zirkel defect major 1.1 front 276 parser test failure zirkel defect major 1.1 front 277 NullPointerException in ModelEnvironment defect major state 279 string parse error in TreeParser zirkel defect major 1.1 front 280 two return locations defect major 1.1 front 281 parser rejects abstract functions which return arrays defect major 1.1 front 282 Null pointer exception in TreeParser: fcn zirkel defect major 1.1 front 283 Dimension mismatch in array declaration defect major front 284 Grammar ignore zirkel enhancement major 1.1 front 285 Automatically cast arrays to pointer expressions zirkel enhancement major ast2model 286 Allow expressions with side effects enhancement major front 287 Support compound statements enhancement major front 288 Support arbitrary nested scopes Stephen Siegel enhancement major 1.1 model 289 Allow function prototypes enhancement major front 290 Add support for preprocessor function-like macros enhancement major front 291 Ignore lines beginning with '# ' enhancement major front 293 Handle casts in simplifier defect major simplify 296 add AST type: Vector stachnik enhancement major 1.1 ast 299 TypeReferenceNodeIF should extend TypeNodeIF zirkel defect major 1.1 ast 300 change type in AST factory composite node method zirkel defect major 1.1 Administration 301 AST root node: override child zirkel enhancement major 1.1 ast 302 add insertChild method in SequenceNodeIF zirkel enhancement major 1.1 ast 304 New command line options Stephen Siegel enhancement major front 306 Function definitions need to be set stachnik defect major ast 307 Error in XML output tmcclory defect major clang 308 Main needs to be included in the GlobalScopeNodes stachnik defect major ast 309 Relax main method signature requirements task major model 314 ArrayIndexOutOfBoundsException in morph (via state) Stephen Siegel defect major 1.1 state 315 Set source file when constructing AST nodes stachnik defect major 1.1 ast 316 Add representation of comma operator to AST stachnik defect major 1.1 ast 317 failure on example.c defect major 1.1 multiple 318 Add Assignment Type Field to AssignmentNodeIF stachnik defect major Administration 319 Add Support for Multiple Inheritance to XML Schema stachnik defect major XML 320 PragmaNodes should be GlobalScopeNodes stachnik defect major ast 321 Make ASTTransformer to find startof nodes zirkel task major ast 322 Update Clang XML LoopNode Output tmcclory defect major XML 323 Array Extents Not Specified in Clang Output tmcclory defect major clang 324 Add source information to function body tmclory enhancement major clang 325 Set source for implicit return. zirkel enhancement major ast2model 327 Add key-value annotations to AST nodes stachnik enhancement major ast 329 Generate Human-Readable Description of XML Schema stachnik task major XML 333 Bug in MorphicSet.contains()? Stephen Siegel defect major morph 334 Simplification of function application defect major symbolic 24 symbolic arrayWrite method giving incorrect results ywei defect critical symbolic 38 Need ifThenElse symbolic expression ywei task critical symbolic 160 "Prepare ""binary"" release" zirkel task critical Release 1.0 Administration 167 Upload binaries Stephen Siegel task critical Administration 292 bug when initializing multiple variables in one decl Stephen Siegel defect critical 1.1 front