Context Navigation

Timeline

09:10 Things To Do edited by zirkel: (diff)
09:04 Ticket #205 (Extend evaluateLiteral in Evaluator to support records, arrays, and ...) closed by zirkel: fixed: Done.

21:07 Ticket #211 (don't check for deadlocked states when not necessary) created by Stephen Siegel: No need to check for deadlock at a statement that can't block, like an …

16:01 Ticket #209 (Add support for APPLY operation in CVC3TheoremProver) closed by ywei: fixed: Operation support added in CVC3 theorem prover class.
13:13 Ticket #207 (Add support for APPLY to CVC3TheoremProver) closed by ywei: fixed: There is a duplicated ticket for this issue assigned to me and I will …
13:11 Ticket #204 (Allow array type variables to have initialization) closed by ywei: fixed: Changes made. Variables of all types are allowed to have …
13:11 Ticket #203 (Add support for record and array literal expressions to the front-end) closed by ywei: fixed: Features added. Front-end supports array and struct type …
09:54 Things To Do edited by zirkel: (diff)

12:15 Things To Do edited by Stephen Siegel: (diff)
12:14 Things To Do edited by Stephen Siegel: (diff)
12:11 Things To Do edited by zirkel: (diff)
11:45 Things To Do edited by Stephen Siegel: (diff)
11:29 Ticket #210 (Try to build solaris version of CVC3, etc.) created by zirkel: We'd like to build on the webserver. Otherwise maybe we can switch it …
11:23 Ticket #209 (Add support for APPLY operation in CVC3TheoremProver) created by ywei: Add support for APPLY operation in CVC3TheoremProver.java. The …
11:22 Ticket #208 (Separate pragma parsing out of language parser and put it into model ...) created by ywei: The "#pragma" representation need to be separated from the language …
11:19 Ticket #207 (Add support for APPLY to CVC3TheoremProver) created by zirkel

11:36 Ticket #206 (Formal grammar for assertion and joint invariant language) created by zirkel: We need to write this down.
11:13 Ticket #205 (Extend evaluateLiteral in Evaluator to support records, arrays, and ...) created by zirkel: Need to call the right methods in the dynamic factory. Arrays/structs …

19:13 Ticket #204 (Allow array type variables to have initialization) created by ywei: In …
13:15 Ticket #177 (Add record literal expression in model package) closed by zirkel: fixed: Implemented. This is called recordLiteralExpression to be consistent …
13:13 Ticket #173 (Add char type to model and value layer) closed by zirkel: fixed: Implemented.
13:13 Ticket #203 (Add support for record and array literal expressions to the front-end) created by zirkel: There are methods in the ModelFactory called arrayLiteralExpression …

10:18 Ticket #200 (compilation error in model module) closed by zirkel: fixed: Sorry about that, I had made both changes but accidentally only …
09:44 Ticket #202 (installation from source) created by Stephen Siegel: Can someone summarize for me how to a. install gmp, 64 bit version. …
09:19 Ticket #201 (source release) created by Stephen Siegel: I downloaded TASS source release latest and there are a number of …
09:12 Ticket #200 (compilation error in model module) created by Stephen Siegel: Looks like ModelFactory was changed, but not ModelFactoryIF (or vice …

21:01 Ticket #199 (CVC3 prover does not handle MODULO) closed by ywei: fixed: Operation support added. The skew factor example now works.
15:30 Ticket #185 (Verification Suite) closed by zirkel: fixed: Done. The trac is at vsl.cis.udel.edu/trac/fevs

23:38 Ticket #199 (CVC3 prover does not handle MODULO) created by Stephen Siegel: Need to add handler for MODULO is the prover.

11:24 Ticket #197 (linear time membership test in loop module) closed by ywei: fixed: Use the containsValue() method now to test membership now instead of …
11:22 Ticket #174 (Print intermediate report during execution) reopened by Stephen Siegel: Not sure if this is best way to do this. Also, has not been applied to …
11:12 Ticket #173 (Add char type to model and value layer) reopened by Stephen Siegel: Still need to implement arrayLiteralExpression, …
10:24 Ticket #173 (Add char type to model and value layer) closed by zirkel: fixed: Character type is represented at the model and value layer. At the …

12:43 Ticket #139 (running simpleRecordTest causes freeze) closed by Stephen Siegel: worksforme: No longer causes freeze, but has another problem (separate ticket opened).
12:42 Ticket #198 (PointerTest: record test has infinite recursion) created by Stephen Siegel: Test pointers/PointerTest.simpleRecordTest fails because of an …
00:15 Ticket #194 (nestedLoops: inconclusive result in v1.0) closed by Stephen Siegel: fixed: Fixed. There were so many bugs it would be difficult to list them …

23:14 Ticket #197 (linear time membership test in loop module) created by Stephen Siegel: The following code is in loop.StateFactory.java. This is not the …
19:00 Ticket #190 (Add list of abstract functions to XML representation of model) closed by ywei: fixed: Abstract function list added in the XML schema.
18:16 Ticket #195 (missing diffusion_par.mmp) closed by ywei: fixed: I copied the diffusion_par.mmp from v0.9 to the directory.
18:14 Ticket #174 (Print intermediate report during execution) closed by ywei: fixed: Intermediate report added. Program will print out a short message for …
18:13 Ticket #196 (source still too big) closed by ywei: fixed: Fixed. Condition statement now only displays the guard expression …
11:02 Ticket #196 (source still too big) created by Stephen Siegel: This is in the test good in the FibTest. Complete body of if …
10:56 Ticket #195 (missing diffusion_par.mmp) created by Stephen Siegel: diffusion_par.mmp is missing from examples directory in v1.0

15:02 Ticket #171 (Multiple improvements to binary release) closed by zirkel: fixed

09:54 Ticket #194 (nestedLoops: inconclusive result in v1.0) created by Stephen Siegel: Can you take a look at the nestedLoops example and see if you can …

22:12 Ticket #193 (source text for loop too big) closed by ywei: fixed: Fixed. The loop statements and function now only display the header …
21:49 Ticket #193 (source text for loop too big) created by Stephen Siegel: The source text for the while loop includes the entire loop body. It …
21:21 Ticket #192 (string index error in parser) closed by ywei: fixed: Fixed. All existing example tested by JUnit test using ParserTest …
21:05 Ticket #192 (string index error in parser) created by Stephen Siegel: In cycle.CycleTest: […]
14:53 Ticket #191 (source text not set correctly) closed by ywei: fixed: Fixed. I modified the way the source information is calculated and I …
11:27 Ticket #191 (source text not set correctly) created by Stephen Siegel: Running in verbose on adder example you will see that some of the …

Note: See TracTimeline for information about the timeline view.