Timeline



06/10/10:

17:57 Ticket #216 (Simplifier: improper simplification when simplifying on an implication) closed by Stephen Siegel
fixed: Fixed: enhanced Simplifier by adding method "extractRemainingFacts" to …
14:55 Ticket #216 (Simplifier: improper simplification when simplifying on an implication) created by dfix
I created a simplifier with the assumptions p1 and ~p2 and simplified …
14:20 Ticket #215 (Discrepency when simplifying using reals vs integers) closed by Stephen Siegel
fixed: Fixed: problem was almost nothing was being done to simplify …
12:39 Ticket #215 (Discrepency when simplifying using reals vs integers) created by dfix
Creating a simplifier with the assumption integer x=1 and then …
12:28 Ticket #214 (Simplifier: x=y && y=2 does not simplify correctly on x) created by dfix
Creating a simplifier with the assumptions x=y and y=1, and then …
11:30 WikiStart edited by bperry
(diff)
11:22 C Interface edited by Stephen Siegel
(diff)
11:21 C Interface edited by Stephen Siegel
(diff)

06/09/10:

19:16 Libraries edited by Stephen Siegel
(diff)
12:41 Libraries edited by zirkel
(diff)
12:02 Libraries edited by Stephen Siegel
(diff)
11:59 Libraries edited by Stephen Siegel
(diff)
11:44 Libraries edited by Stephen Siegel
(diff)
00:38 C to tass-AST xml created by bperry

06/08/10:

11:36 Ticket #210 (Try to build solaris version of CVC3, etc.) closed by Stephen Siegel
wontfix: Subsumed by Ticket 212.
09:36 Ticket #213 (Add array and record literals to frontend) closed by zirkel
invalid: You are correct. I was confused because I thought we should be able …
01:29 Ticket #213 (Add array and record literals to frontend) created by zirkel
Support for these literals exists at the lower levels, but is not in …
01:16 Libraries edited by zirkel
(diff)

06/07/10:

23:57 Ticket #198 (PointerTest: record test has infinite recursion) closed by Stephen Siegel
fixed: Solved, with some significant modifications to the value type system, …

06/04/10:

14:18 WikiStart edited by zirkel
(diff)
12:46 Libraries edited by Stephen Siegel
(diff)
12:39 Things To Do edited by Stephen Siegel
(diff)
12:38 Libraries edited by Stephen Siegel
(diff)
12:36 Libraries edited by Stephen Siegel
(diff)
12:34 Libraries created by Stephen Siegel
12:25 Things To Do edited by Stephen Siegel
(diff)
12:22 Things To Do edited by Stephen Siegel
(diff)
12:17 Things To Do edited by Stephen Siegel
(diff)
12:09 C Interface edited by Stephen Siegel
(diff)
12:01 C Interface edited by Stephen Siegel
(diff)
11:58 C Interface edited by Stephen Siegel
(diff)
10:57 Things To Do edited by zirkel
(diff)
08:21 Ticket #212 (move auto tests to anton) created by Stephen Siegel
The auto tests are currently run on ludwig. These should be moved to …

06/03/10:

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.

06/02/10:

10:32 C Interface edited by bperry
(diff)
09:59 Things To Do edited by zirkel
(diff)

05/27/10:

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 …

05/24/10:

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)

05/21/10:

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

05/18/10:

09:25 Things To Do edited by Stephen Siegel
(diff)
09:08 Things To Do edited by Stephen Siegel
(diff)

05/17/10:

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 …

05/16/10:

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 …

05/15/10:

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 …

05/12/10:

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

05/11/10:

23:38 Ticket #199 (CVC3 prover does not handle MODULO) created by Stephen Siegel
Need to add handler for MODULO is the prover.
Note: See TracTimeline for information about the timeline view.