| #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
|
| #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
|