/[eiffelstudio]/branches/eth/eve/.gitignore
ViewVC logotype

Log of /branches/eth/eve/.gitignore

Parent Directory Parent Directory | Revision Log Revision Log


Links to HEAD: (view) (annotate)
Sticky Revision:

Revision 91379 - (view) (annotate) - [select for diffs]
Modified Fri Mar 15 08:48:07 2013 UTC (6 years, 9 months ago) by jasonw
File length: 6 byte(s)
Diff to previous 87409
<<Merged from trunk#91375.>>

Revision 87409 - (view) (annotate) - [select for diffs]
Modified Wed Oct 5 07:58:20 2011 UTC (8 years, 2 months ago) by wests
File length: 2798 byte(s)
Diff to previous 86265
Squashed commit of the following:

commit 46e41ab73f9097855de441b20f11a3e137bab0a5
Merge: be0b3a9 8b39ba3
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Oct 4 16:21:35 2011 +0200

    Merge branch 'master' into demonL_inst

commit be0b3a95afa1b2292de26525f57fad4b1f8d3d44
Author: Scott West <scott.gregory.west@gmail.com>
Date:   Sun Sep 25 19:12:24 2011 +0200

    Fixing translation to demonL.

    Old translation didn't set the feature, so feature arguments couldn't
    be resolved to types.

commit 94d6de13bc19bc90d9de5d2fa685244f5fb1bae7
Merge: e128d41 26f3458
Author: Scott West <scott.gregory.west@gmail.com>
Date:   Sun Sep 25 14:16:06 2011 +0200

    Merge branch 'demonL_inst' of bmse-pc251.inf.ethz.ch:/home/scott/src/eve into demonL_inst

commit 26f3458c7ceb8e55289e32ab8308e91795273de9
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Sun Sep 25 14:15:47 2011 +0200

    Adding locals to exported state.

    Still have to restrict them to be mutation free.

commit e128d41204763fdc8e1aa83256d7235fec91b9f9
Merge: 19c8e5a e8fff36
Author: Scott West <scott.gregory.west@gmail.com>
Date:   Sun Sep 25 14:14:37 2011 +0200

    Merge branch 'master' of bmse-pc251.inf.ethz.ch:/home/scott/src/eve into demonL_inst

commit 19c8e5a43bc550445e4bc0f18cf96696a9684ffd
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Sep 21 20:08:07 2011 +0200

    Adding check processing.

    Also adding a convenience function to SSA_SHARED.

commit 1a705d6bd19184c3efb750ba854fb8160c18994f
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Sep 21 20:07:37 2011 +0200

    Allowing old in the body if using the deadplan.

commit 417273f36286741f667ea6c90c610d2cf0208633
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Aug 29 14:42:01 2011 +0200

    Slightly more readable output of goals.

commit 0626e0ddcffb254fd700afb4f33c19c2cfbd2199
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Aug 29 14:41:41 2011 +0200

    Don't both with the sorting of classes.

commit 5153b50f44faf8d5c33f11372cd99754c70994f3
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Aug 19 16:24:06 2011 +0200

    Added new instrumentation and ignored classes.

commit 9041564e8956e734cc3c8035e1650e13a2eca6e6
Author: Scott West <scott.gregory.west@gmail.com>
Date:   Wed Aug 17 07:56:46 2011 +0200

    Re-inheriting SSA_SHARED.

commit 3b5dfa1d9fdf778b3127882d1d56fe1454012547
Merge: 23752e1 0218cc4
Author: Scott West <scott.gregory.west@gmail.com>
Date:   Sat Aug 13 11:32:04 2011 +0200

    Merge branch 'demonL_inst' of bmse-pc251.inf.ethz.ch:/home/scott/src/eve into demonL_inst

    Conflicts:
    	Src/framework/ssa-ifier/expr/ssa_expr_nested.e
    	Src/framework/ssa-ifier/ssa_class_to_demonl.e
    	Src/framework/ssa-ifier/ssa_domainifier.e
    	Src/framework/ssa-ifier/ssa_expr_fixer.e
    	Src/framework/ssa-ifier/ssa_feature_printer.e
    	Src/framework/ssa-ifier/ssaifier.e

commit 0218cc4840e1b5a051b45d4fbb530981ce692109
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Sat Aug 13 11:14:58 2011 +0200

    Adding backup files to gitignore

commit 9475d1841a986fa38f935f64f80fcd137f03f6fc
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Jul 27 10:14:35 2011 +0200

    Adding default (true) rely condition.

commit 0b95538c1ea987fc865fcb518acb08e9e97f8ed6
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Jul 27 10:14:13 2011 +0200

    Adding loop processing, line number tracking.

commit b549a2b776882b5e0ae06424d820e9e7379c9915
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Jul 27 10:13:40 2011 +0200

    Removing debugging ouptput.

commit 9ea5bd006e31893b14e569e9e6fbf698c22a21ca
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Jul 27 10:13:00 2011 +0200

    Using semistrict operator.

commit 34ea8dac90ecc31f62dc92dacbaa4e9c1559a9f6
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Jul 27 10:12:27 2011 +0200

    Adding simple attachment postcondiiton.

commit d5db3795ee13703ef4844226a25214ac425590c3
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Jul 22 10:11:02 2011 +0200

    Fixer now correctly catches access_feat_as locals.

commit 38408fda5ca9f324e1d48cd2f82e0b5c0e515060
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Jul 22 09:59:47 2011 +0200

    Removing debug line.

commit dc92baeb3cb90b6dea9a216de50fbdf3c9241f9e
Author: Scott West <scott.gregory.west@gmail.com>
Date:   Mon Jul 18 10:38:28 2011 +0200

    Actual arguments to nested are now `old'.

commit 86a1c0d72c8b687c8e1d5ad827f58137e2601d0c
Author: Scott West <scott.gregory.west@gmail.com>
Date:   Mon Jul 18 10:37:48 2011 +0200

    Another type of expression that can be processed.

commit f193882feb26872ef13f29085a884b02aa3009ab
Author: Scott West <scott.gregory.west@gmail.com>
Date:   Mon Jul 18 08:49:11 2011 +0200

    Restoring the feature to process

commit b868ee9317c23742850cee572590eb81fa48e34b
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Jul 14 14:58:24 2011 +0200

    Adding Result and create expression support.

commit 14705a65cf5c89badd1ab19ffdbb2d5a45eeb6a8
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jul 12 14:30:08 2011 +0200

    All classes now go in a single domain file.

commit 8c7ebc0b25f3eaed62733f2e642cca8696b66d34
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jul 12 13:59:37 2011 +0200

    Fixed: Current wasn't part of the argument list.

    The argument attributes were being used in the loop, however, this should
    have actually been their copy, with the Current variable as target.

commit 9a7f92a425f93841300203c7d3a4cf4417e56283
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jul 5 10:21:56 2011 +0200

    adding optional prefix to printed variables

commit be97e947c97a9a3d91b2a92d8ce271f33f767dff
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jul 5 10:09:55 2011 +0200

    Consistent naming of ssa-framework classes.

commit 26e8e2820ad03a12ecf367a9af8d08caa0d70bcf
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jul 5 09:56:09 2011 +0200

    Fixing output of boolean constants.

commit a001b68fbb2950154c27c7ebdb980f50c0deb206
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Jun 27 16:43:33 2011 +0200

    Another step towards demonL generation

commit e1879a44d6b8c47e921857613e5a0a5b2a10fd65
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jun 21 13:46:16 2011 +0200

    Totally removing sexpr library.

    Also removing all remaining mentions of sexprs, obviously.

commit 0b26abdae14f23561fd8488efa97c24c6946f7f6
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jun 21 13:39:58 2011 +0200

    Removing mentioned function.

    This was only for frame conditions, which are now handled in the demonL
    language.

commit b096b975d45f21ff2a81a3ff3639bbe8e6b97bf6
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jun 21 13:31:18 2011 +0200

    Renaming skeleton for domain generation.

    In preparation to do demonL domains.

commit db2be3b279746c41cfb33e0450be54964863d6e7
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jun 21 13:28:59 2011 +0200

    Taking out most YICES specific pieces.

    These will be replaced by string generation for demonL.

commit 6b626ee406389fe2aa9a7da2df245312178dc842
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jun 21 08:50:57 2011 +0200

    Last commit before abandoning a lot of code.

commit 3942e6730f1e7e8c2a7e709856b9a7613151b91e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri May 6 17:12:32 2011 +0200

    Restructuring frame conditions.

    Switching to an implication style which should allow finer-grained inferred
    frame conditions.

commit e09564b968f31893d5a533fb3821183a6ba3b843
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon May 2 13:04:16 2011 +0200

    Adding non-void precondition.

commit 41c765e24270beb4fbf48bba8af7b8faa861a401
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon May 2 13:04:06 2011 +0200

    Removing debugging print.

commit 3bdb5f68847396e14bc0c959b3d811c4d38fa4fb
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Apr 19 15:03:07 2011 +0200

    Organizing ssa_shared, fixing the rely.

commit 0516e806930f37575ae7d358785dd701e1187d02
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Apr 19 13:39:47 2011 +0200

    Add contracts, more post-condition processing.

commit 507b7a8a167b3366db37a5f53801df846562be92
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Apr 8 09:52:11 2011 +0200

    Refactor exprs, fix frame condition.

commit e5babdeb8bf19e8616bd791e4498c8d7005a8fab
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Apr 4 16:33:46 2011 +0200

    Adding Void values for references.

    Also adding appropriate preconditions about void.

commit a46cb327e569413ab7c0a16a144dafb49cc02240
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Apr 4 16:33:00 2011 +0200

    Ignoring temp files.

commit 363cbc53bc81e0795575eb1bea2acfb663bca56c
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Apr 4 11:15:05 2011 +0200

    Adding multiple supplier processing.

commit 5c1cd68f002ddd610f1bf48d6a71a3af8a79dc6d
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Apr 1 16:26:34 2011 +0200

    Fixing rely clause generation.

commit a0cb13dfd30bd7518dcfd028e9319189d77b6ec9
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 29 11:11:12 2011 +0200

    Fixing output of frame-related expressions.

commit 6fe0dc344ac1d1deee3ee55b18c184aabac7ad00
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 28 16:16:20 2011 +0200

    Pre-cond extraction now maps Current appropriately.

commit 13bb54d3ffeb31b4f994ffbf2807627558d3bc70
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 28 16:04:19 2011 +0200

    Refining frame functions.

commit 98fd1f81b5645a1ce2b28ae8b4388f3ab4fd6c26
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 28 09:38:44 2011 +0200

    Shifted all domain tag/ref generation into a single file.

commit d81141337a8aa059c43734c877ca034ef40bde60
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 22 15:03:13 2011 +0100

    Adding 'mentioned' generation.

    This is used to generate frame conditions which can exclude
    certain objects (ie, the mentioned ones).

commit ff5ccd278c80f0e5854252b9a9d12ba60d295c53
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 22 15:01:57 2011 +0100

    Domain generation produces general yices file.

    The general yices file pulls together all the type definitions
    and wraps them.

commit 12251e9185aa1847548d9eec359cd5e684d7e1d5
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 22 11:07:03 2011 +0100

    Fixing shared feature global implementation.

commit 929caab94efa4a661a5f5dae25f09544fb696dbe
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 22 10:30:22 2011 +0100

    Adding a mentioned query.

    The mentioned query pulls out all variables that are mentioned
    in an expressionn.

commit 3e63d0993d9fbd0e77f6c9024d7acdfe59122e5c
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 21 14:57:49 2011 +0100

    Generation action for a single class.

commit b60e71a3d9400163fd5f4ece9865f034b0d91bf2
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 21 14:57:24 2011 +0100

    Suppliers processing args, tags, refs-wrapping.

commit 2069c880a94ee71745eeca94b040db41c6efebda
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 21 13:39:21 2011 +0100

    Reorganizing s-expr util, adding supplier processing.

    Some changing around of where the utility functions for s-exprs live.
    Also introducing generation of the module to gather supplier data together
    so more than one class can be used for planning.

commit 9800f9f14081bcc90c7d5abdaa991fde308102b1
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 21 13:11:23 2011 +0100

    Yices generation involving all suppliers.

commit 83457763f2d368f8bf8cd304ee952c6de156e012
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 21 10:14:53 2011 +0100

    Organizing a few features into sections.

commit c6bdbf5d3943b24638f34216edf27ba77879362e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 21 09:39:49 2011 +0100

    using the prefixed_name function

commit 154e06e092503c5572508014ddc154b968a18595
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Mar 18 13:13:07 2011 +0100

    Move some functions to standalone sexpr library.

commit ec817b145ac7b74dcac674a7b3c19ff2471329d0
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Mar 18 10:35:47 2011 +0100

    Adding equality generation sexpr utility.

commit 89c09ad77629d1e06d9b6a0909db7c176e086df8
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 17:07:04 2011 +0100

    Removing unused classes from old instrumentation.

commit 1ae7361d0fb27d510ddea70ab818a7a6f9d1c1d8
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 16:03:29 2011 +0100

    Inserting call to rely_plan in generated code.

commit 05ac9f9aa9fbb52e5d7570f1c266aa15428fb3d1
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 14:40:11 2011 +0100

    Change name to 'instrument', more descriptive.

commit 282cc303984899fbb6b3d68bacce1dc4c2386cd2
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 14:25:41 2011 +0100

    Process ifs and assignments in ssa printer.

commit d5fbb837560fc6e024aea661dbf78d7abe88b600
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 14:25:18 2011 +0100

    Fix pre-conditions of attributes as 'true'.

commit 12f7b3c74002bda85507879f21107a47737d33c0
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 11:24:39 2011 +0100

    Fixing double-output of precondition, cleanups.

    Unnecessary variables related to the old approach have been removed.

commit 79d5d363a0aaa74178a836a5a3eccca07af4694f
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 10:29:16 2011 +0100

    No need to save shared feature_i.

commit 335f94687f69e9872c1557cdbd3c68747ea81b85
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 10:28:51 2011 +0100

    Detabifying feature printer.

commit 1f3bab3629bfd892d38bfe9637d543f0adeedf65
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 16:41:26 2011 +0100

    Preconditions can now be instantiated properly.

    Before, the expression generation worked only for non-instantiated
    arguments, but now those can be mapped to particular expressions
    (actual arguments).

commit d140890a5b86c2465ed8aaa95e78c71d092310a2
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 15:15:54 2011 +0100

    Removing unused local.

commit 2d65e91f6e093553dc030d3bb1a74647ca7b19f3
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 14:57:51 2011 +0100

    untabifying

commit cf907ad87b2ae05372d6aaace7d58b9192e2e45e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 14:57:21 2011 +0100

    Formatting update.

commit 1e1212c3ddb2ded0af811517ab53dff6a7b76edd
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 14:46:38 2011 +0100

    Removing the usage of the ARRAY.

    Replaced this with an ARRAYED_LIST which allows for much cleaner code.

commit 2a8c6d62ab18352e4b4f7fdc37fd1e40f8beb6a3
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 14:36:40 2011 +0100

    Removing additionally unneeded checks.

commit 524d51e48168b0823f0586af5ac58c986587193d
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 14:33:48 2011 +0100

    Removing  initial Result+, result is initially Void.

commit 434a2f8e624c1e09c66455bca3045b8fadd36bb8
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 14:33:03 2011 +0100

    Removing void-branching code, target is always attached.

commit 0537a8eb6223bfbd6021e2ac5fa63504c45e4ec9
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 11:18:41 2011 +0100

    Further removal of old replacement scheme.

commit 936107a57e72cea11d278ee111442046f9931b13
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 11:07:50 2011 +0100

    Removing printed_locals flag.

commit b0e3d378e13b639d11082bfbe772884ee834b0c0
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 11:06:12 2011 +0100

    Continuing to clean out old instrumentation.

    Locals are no longer added, for instance.

commit 4b4d53d3fc2169cdc01553941f82c34ab738485b
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 10:59:42 2011 +0100

    Reworking the expression tree slightly.

    The tree now demands that nested calls have a non-void target.
    To fill this in a new node has been created to take the place of
    Current, (we call it "this" to avoid name overloading).

    Some old replacement code is being stripped away as well.

commit 08cf8cc538061deb639cd36c46e089fbf60ae661
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 10:06:13 2011 +0100

    Adding creation precondition, simplifying all_pre_conds.

    The precondition on the creation procedure should enforce that the
    variable is not a feature, but a true variable (formal argument or local).

    The all_pre_conditions now returns an empty list.

commit 49ab98183dff57585a4c003611f2040f7f4d4a96
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 10:01:44 2011 +0100

    Formatting update.

commit e0946eb8089bf260668a5085905494d6e3eadcf3
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 14 17:38:20 2011 +0100

    Formatting update.

commit 4ff4ec496f8469d8c3a8502707d6084fe7b2c611
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 14 17:27:13 2011 +0100

    First step towards simpler instrumentation.

    Preconditions are extracted from syntax trees and turned into a list
    of s-expressions.

commit 54516ee6de6c49b9fbdc3c51526ba69a1bdd558c
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 14 16:04:50 2011 +0100

    Detabifying ssaifier.e.

commit e0ea75c916fafa31ee0aeae9c65ee37f1120eaf7
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Mar 9 09:47:01 2011 +0100

    Reworking the index lambda.

commit 6622ce763ec3e6096064827afc4efd635f24b427
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Mar 9 09:46:15 2011 +0100

    Fixing boolean output, lower-case only.

commit 7d17b4b7baad3e84c328c4cb3c439f9c9c27a594
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Mar 9 09:44:56 2011 +0100

    Fixing once would should have been a 'do'.

commit c2c3e58e0517ebb403fd109bf9c3983f371b32b3
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Mar 2 13:28:10 2011 +0100

    Generating frame only after functions and attributes.

commit a63df48b1f67cf60cf131c91299a9cc3b67df407
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Mar 2 13:26:56 2011 +0100

    Changing delcaration generation to omit parentheses.

commit ad4ddf111b3d6a14b2cd7d269a87ca12707174f5
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Mar 2 12:39:03 2011 +0100

    Using BOOL_AS.value now to get literal boolean.

commit 116c6364751b9b67b9d06cebf6fe4d3bbf621da2
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Mar 2 11:18:00 2011 +0100

    Process `Result=' style funcs, fix index in procedures.

    Adding a few utility function to generate the indexed-lambda,
    and changing the name of the attribute_name to a more general
    prefixed_name as it will work on any type and string.

commit 6c59b3073b23c8c4084db314b0b3f0dda8221292
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 17:02:39 2011 +0100

    Add stub generating lambda for Eiffel functions.

commit e6aa668148482a8baacc7f8ebb7445a68801df63
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 17:00:22 2011 +0100

    Updating variable name in mk_lambda.

commit cbb668547f74c849a8a390a2620b164fb2c8b4a2
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:44:50 2011 +0100

    Formatting update.

commit 3ab5b118cad92d4d66a3155b91d0a1bd18ce60b2
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:35:35 2011 +0100

    Setting the shared feature_i from the domain generation.

commit 5c0335097037de74b52e53a1012c465f9d3b8a65
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:34:52 2011 +0100

    Nested features now use `type.

    Also added a new feature which gets the type of the target, as it can be
    Void is must be treated specially.

commit b89bbb7f7dec42a8b53eefbcc759a52a2c074461
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:34:29 2011 +0100

    SSA_EXPR_VAR now uses the `type' feature.

commit e66aaa4f11d6875d53beff8b0318fe62ea1f1dba
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:33:53 2011 +0100

    Overriding new type feature when the operator is `old'

commit c36075471aa52ea0567ff4fa2dde1778b4062ba6
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:31:21 2011 +0100

    Adding a `type' feature to SSA_EXPR.

commit 4aa4c45a439429a1dcfef0f66085ce2870f15a99
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:29:58 2011 +0100

    DOMAINIFIER now uses SSA_SHARED

commit cf65f3eb10e838f48feac2f5f62b6790f389fefa
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:29:24 2011 +0100

    Using a CELL internally in SSA_SHARED.

commit c611cfe89dc62d5def41608782476e104be0fbff
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:29:05 2011 +0100

    Removing debugging print.

commit 718ede55272af0cacf82cca9231e58ed16085377
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 12:01:10 2011 +0100

    Fixing indentation: spaces -> tabs.

commit c6d2b0ef6029227d88b5e615f1856d9150eda220
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 10:09:53 2011 +0100

    Adding conversion function from classes to names.

    This makes it possible to remove generic arguments from types. Any function
    which was generating its own prefix based on classes now uses this.

commit e1549a54126f34fe5b407dcdc058535830b34a09
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 09:18:51 2011 +0100

    Adding frame generation, name conversion utilities.

    The name conversion utilities are to try to combat some fragility in the
    way names are generated.

commit a3c21669b6acf4303443747bd5c0d3e980d23972
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 08:46:10 2011 +0100

    Formatting changes.

commit ff4866f3388a494b48930e0ee28b232daae0ac6b
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 24 11:20:04 2011 +0100

    Off by one in "this"-prepended arguments of a nested call.

commit 6630e6399581fdd5f99caeda8d4f84d8ed6384f0
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 24 11:13:28 2011 +0100

    Ignore class invariant processing.

commit d5b373da96f6e1fe8a97c818492df288377c0ff7
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 24 11:12:05 2011 +0100

    Check-false -> print TODO for converting functions.

commit de50c955a318ab7dd05f89ef04e38b407fd0a750
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 14:55:55 2011 +0100

    Cleaning up small items.

commit fc426478d612547e2fd5255d722a6cd61a173a80
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 13:52:11 2011 +0100

    File output using domain_string from the yices domain class.

commit 52e0299c16825c7de0e7f5316e1b3adbee069c33
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 13:51:22 2011 +0100

    New feature to convert class to yices string.

commit bbd76d74028bd64231ce69dd224dbe044f53875d
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 13:45:14 2011 +0100

    Output the domain now into a file, rather than stdio.

commit 1de673368894763300cbb2d6d38b0e28a367c123
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 13:04:50 2011 +0100

    Generate action tags.

commit 4c43b40d63279e1e1cb629b2bd2d68bc5c910ce7
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 12:57:18 2011 +0100

    Adding define_type and mk_scalar functions.

    These are now used to reformulate the temp objects for a given class.

commit 69c0e4d5c4152849658edd8ac6e4d7bd5c23efff
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 11:18:06 2011 +0100

    Using the mk_and utility function.

commit 28e785d7c98470e6585181a974086ee5072666fa
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 10:15:36 2011 +0100

    Updating formating.

commit 67ffe587a64574e273bc486d6a1468266c23539e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 09:49:32 2011 +0100

    Using mk_list in ssa nested expressions.

commit f468178133f2c62a5660136083d9f1d76967ce6f
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 09:48:55 2011 +0100

    Now using mk_list in yices domain generation.

commit df65ef57db0871f474c3e37ccde965e5d2bb1aeb
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 09:48:01 2011 +0100

    Using now mk_list in yices utilities.

commit e44c209068e383666de1e7b72d494094bc2456ae
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 09:47:03 2011 +0100

    Updating declaration generation.

    Removing the outer parenthesis to be more in line with what YICES uses for syntax.
    The other may have worked, but this seems more idiomatic from the documentation of YICES.

commit f6c8e7ad7bd2aff3cb460b22d24113dc34183fd9
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 09:44:42 2011 +0100

    Adding mk_list s-expression utility.

commit 50569673a15eba7df06a670abb3d84dbc62fce3e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 17:19:06 2011 +0100

    Refactored ssa_yices_domain.

    The common yices functionality now lives in a utility class,  allowing
    the domain construction class to be much smaller and cleaner.

commit 7347c8a49367c45ce35462cfc3186cbe1db24ac7
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 17:18:47 2011 +0100

    Domainifier now prints out the yices domain.

    This is just a temporary thing so it can be seen easily while worked on. The output
    was moved here so that the ssa-yices-domain class could be cleaned up.

commit 89ce35251c91b4a6465abf630054d3daa75d22d3
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 16:23:43 2011 +0100

    Changing static type of empty_list to ARRAYED_LIST.

commit 43a56ce9c8fe1e991be9625816a572a47258d389
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 16:21:50 2011 +0100

    Domain now returns a single sexpr.

    Debugging printing of the class domain has now been removed as well.

commit 76f08ee37dccf7573523391aaaa4a1fcfe4af100
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:52:00 2011 +0100

    Removing obsolete feature call.

commit 42180cebc9c509f126030cb09346af51baf16c6f
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:46:33 2011 +0100

    Fixing function calls with indices.

    Now the indexes are used to form the function call, before
    they were omitted.

commit d301a515d3ef4464f6039c6299b20b7db99b2ecc
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:45:06 2011 +0100

    Enhancing expression fixer.

    The fixer now incorporates the argument list so it can distinguish
    formal arguments from unqualified calls.

    Related updates have been made in the clients.

commit 70fd0f90a60596aab8c3ba36649fec662778e0a6
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:18:47 2011 +0100

    Untabing expr_fixer.

commit ed3de15f2ec344c6fff6ae376bab3ed6b76e3162
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:09:37 2011 +0100

    Fixing runtime crashes and some output bugs.

commit c8f4624820b8b38f6d6e4f5c437f1086c12149b4
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:09:19 2011 +0100

    Adding invariants to class descr.

commit 61e940be11b0400e15b85e4cc9d773373c551266
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:07:50 2011 +0100

    Inserting calls to yices domain conversion.

commit 1759b3c75574b83df509bcf7e9d57ffbeb1a6e91
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:07:22 2011 +0100

    Including invariants in declarations.

commit a8aa500470e15bfc03f9c73e939cb75e03c50e4d
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:06:59 2011 +0100

    Initializing arguments list in feature descr.

commit d672fcb007766d96328372e9831cf28f2e82f465
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Feb 21 17:07:43 2011 +0100

    Class-to-yices pre-post condition conversion.

commit 097e27cb3bed2eaee44feb0aa9594e40706bc5de
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Feb 21 16:37:28 2011 +0100

    Add function to translate args to types.

    The argument declarations are taken in combination with the target type
    to generate a type declaration that includes all names/types.

commit 6d29954ed711e5e1f062006fb226f2ca75fa0708
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Feb 21 15:36:54 2011 +0100

    Cleaning, adding some skeleton implementations.

commit ee040cd44f42a8f211f76687eb5648503304b111
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Feb 21 15:36:17 2011 +0100

    Updating ssa expressions to convert to sexprs.

commit 1579958642576d0f14ee242ae5ce9e486d283487
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Feb 21 14:30:20 2011 +0100

    Updates to yices domain conversion, sexpr utils.

    The class description is now based on type, not name. Suitable updates
    have been made to the higher-level classes to use this convention.

commit 3246b240ab50b942659a49a9c33412d20a533ad9
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 18:05:42 2011 +0100

    Adding utility and ecf for sexprs.

commit 4898c3fc23f2c0bf316eb0cb4106ad1d7fe1a278
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 18:04:39 2011 +0100

    Skeleton of description to domain transformation.

commit f3800c47c5c7bfe7b594723c9848a0b930602f66
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 18:04:04 2011 +0100

    Adding yices domain class to class transformation.

commit 35d798036286936f959467ad6d566788d37d2c2f
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 18:01:07 2011 +0100

    Fixing for new sexpr class.

commit 4b506c62691ac36a3b4330dda807f8bb9acd9411
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 16:36:38 2011 +0100

    Converting to use sexpr library.

    This change is part of the move to yices as a planning back-end.

commit fb502e6445c8ffdcc49c5cd3edf8d7ffb9025514
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 15:20:55 2011 +0100

    Fixing typo in sexpr_const

commit 777910df43ab68c68b09327a57c079b414b242fb
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 13:34:48 2011 +0100

    Removing unneeded expression types.

commit ce6182c4a849036e88ef4713369b5374534e5da2
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 13:33:49 2011 +0100

    Renaming expression classes to include sexpr.

commit 7cd65293624df8f6eeec228e3dcf220cf29077db
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 13:30:29 2011 +0100

    Moving sexprs into their own module.

commit a92c5d7fb30e69b0721924f47398a38a375b5e4e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 17 17:16:51 2011 +0100

    Adding yices conversion class.

commit 7bd20b2631b2f22adb08d1f823b1f6d67f8fe81f
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 17 17:16:23 2011 +0100

    Fixing small compile errors.

commit 57c1d058ee67ab1426fa5442b9fa14d8dde8e381
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 17 17:16:11 2011 +0100

    Fixing typo.

commit c45a4c0990eae3dde9780ddc186c2c93a10a3cf9
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 17 16:28:29 2011 +0100

    Adding arguments to feature description.

commit 52f32e23eedb03cdee4e9ef0c2e2a3e053233c43
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 17 16:27:07 2011 +0100

    Yices conversion now generates *_desc classes.

commit f1c352a6a7aaa147939668502d5ef2213bffde27
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 17 14:15:43 2011 +0100

    Adding classes for describing classes and features.

commit 990de73d679dbb01a5426f34164d323f4b5cdd78
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 17 13:57:14 2011 +0100

    Copy of class_to_domain for SMT encoding.

commit 2bd710e1a9c7ce5d5b056d131e2b4865b5ab2196
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 17 13:50:20 2011 +0100

    Renaming inconsistent class/filenamed pre_to_adl.

commit d3fbf4ad78f6c1970c6395989a6aa2028b9b72e7
Author: S <saynte@gmail.com>
Date:   Mon Feb 7 00:07:37 2011 +0100

    Adding back inclusion of target.

    This broke the previous instrumentation.

commit 8cc4a35d9146a6ce2bc55e8548e3722c5c98dfb2
Author: S <saynte@gmail.com>
Date:   Sun Feb 6 22:38:56 2011 +0100

    Adding gitignore.

commit 419125905c43f51b22575a17d75505e97e46b0ab
Author: S <saynte@gmail.com>
Date:   Sun Feb 6 22:17:41 2011 +0100

    Removing parameter serialization.

    This is now taken care of by the arguments, due to the replacement
    in the rely condition we can do this.

commit efe98d796f639b536aee7d96003ae92d256425c1
Author: S <saynte@gmail.com>
Date:   Sun Feb 6 22:15:48 2011 +0100

    Track assignments with a parameter as source.

    When we have an assignment from a parameter, we store it so we can
    update rely-conditions with it.

commit 518b963310844a1e51f4ee4e01b382d0b1c7791f
Author: scott <scott@scott-desktop.(none)>
Date:   Sun Feb 6 18:21:15 2011 +0100

    Initial commit of demonic testing branch.

commit 23752e1c67f81ffa10779784a50b444c87807527
Author: Scott West <scott.gregory.west@gmail.com>
Date:   Mon Jul 18 10:38:28 2011 +0200

    Actual arguments to nested are now `old'.

commit b1ac2779355b014c9415a6b9854ab8f7cd22ae7c
Author: Scott West <scott.gregory.west@gmail.com>
Date:   Mon Jul 18 10:37:48 2011 +0200

    Another type of expression that can be processed.

commit 876980f239766627ab7cc31e35d894c632b9e2c1
Author: Scott West <scott.gregory.west@gmail.com>
Date:   Mon Jul 18 08:49:11 2011 +0200

    Restoring the feature to process

commit 26197d391a2676f2afff7fa63613334e2e95d8fd
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Jul 14 14:58:24 2011 +0200

    Adding Result and create expression support.

commit dbada28ad461703822dde243cf3bac724ad1ec21
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jul 12 14:30:08 2011 +0200

    All classes now go in a single domain file.

commit 70d30d291fabcfd038b3e0fa6da99140a353f6f6
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jul 12 13:59:37 2011 +0200

    Fixed: Current wasn't part of the argument list.

    The argument attributes were being used in the loop, however, this should
    have actually been their copy, with the Current variable as target.

commit 11e47856f38dd2d941dee2924aa226c783b8710b
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jul 5 10:21:56 2011 +0200

    adding optional prefix to printed variables

commit 4034ac8242eb2f699d8795ec58561365392d6ed0
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jul 5 10:09:55 2011 +0200

    Consistent naming of ssa-framework classes.

commit 1235319acc72fbad0504aa85130341e18b24b25d
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jul 5 09:56:09 2011 +0200

    Fixing output of boolean constants.

commit 65873dce6cea25585cfd77da94e56f9c86a5665b
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Jun 27 16:43:33 2011 +0200

    Another step towards demonL generation

commit c8f0360184c93e6347ee6e29742f9486d7ef19e9
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jun 21 13:46:16 2011 +0200

    Totally removing sexpr library.

    Also removing all remaining mentions of sexprs, obviously.

commit 96657cbb23294ff2dc9541651a2364e4a688ad9f
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jun 21 13:39:58 2011 +0200

    Removing mentioned function.

    This was only for frame conditions, which are now handled in the demonL
    language.

commit 43861ac3fec565ee2c099e1a78a5a8de73846c23
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jun 21 13:31:18 2011 +0200

    Renaming skeleton for domain generation.

    In preparation to do demonL domains.

commit cecd3440b523c2f120a667308ce3ccde4f28636a
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jun 21 13:28:59 2011 +0200

    Taking out most YICES specific pieces.

    These will be replaced by string generation for demonL.

commit bba8fd8cc64fd6c47f3e06a32824e57738c6ebcf
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Jun 21 08:50:57 2011 +0200

    Last commit before abandoning a lot of code.

commit b2d87d9d1babd0012ce5de9cb197a493d191af78
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri May 6 17:12:32 2011 +0200

    Restructuring frame conditions.

    Switching to an implication style which should allow finer-grained inferred
    frame conditions.

commit 1d94188e0d9c8c61c656da4b880ec7e029a6df0c
Merge: 3af0264 b58042e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon May 2 14:03:55 2011 +0200

    Merge branch 'master' into simpler_ssa

    Conflicts:
    	.gitignore

commit 3af026488bc3ac7636dcee56abd5569fe66c5230
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon May 2 13:04:16 2011 +0200

    Adding non-void precondition.

commit f8d72cf4274472b1a9c97dd707e88e2c957c9715
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon May 2 13:04:06 2011 +0200

    Removing debugging print.

commit 733ac5c7527bd54c97e820f36fd85c599fb64a58
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Apr 19 15:03:07 2011 +0200

    Organizing ssa_shared, fixing the rely.

commit 693495e6c92f3ca71347b751bb209b71d20ccb2e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Apr 19 13:39:47 2011 +0200

    Add contracts, more post-condition processing.

commit b3c81caeaa5d041a33e776eecdce50b54beb5d4b
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Apr 8 09:52:11 2011 +0200

    Refactor exprs, fix frame condition.

commit 8ba615b7630f6afa4f005065964a706cbd0451e6
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Apr 4 16:33:46 2011 +0200

    Adding Void values for references.

    Also adding appropriate preconditions about void.

commit b500c610e47bc6a4d05eccb96f3a6aff490fa50d
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Apr 4 16:33:00 2011 +0200

    Ignoring temp files.

commit b634be6eb7a702a8091817efa7ee2d8f0586a042
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Apr 4 11:15:05 2011 +0200

    Adding multiple supplier processing.

commit 2609cbd67ed7417450453452d3b458c05cdf2170
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Apr 1 16:26:34 2011 +0200

    Fixing rely clause generation.

commit d13e574eaffa8be301b7a2346d6954996b976c70
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 29 11:11:12 2011 +0200

    Fixing output of frame-related expressions.

commit 4ea505dfd88c0d4bcee66df3f9823f0969ca4d08
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 28 16:16:20 2011 +0200

    Pre-cond extraction now maps Current appropriately.

commit 2ebd30829413669f90100e93192bb6922c4bef9a
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 28 16:04:19 2011 +0200

    Refining frame functions.

commit e3ecb5997a39a7813ecaf6483fbb5b9910b31d86
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 28 09:38:44 2011 +0200

    Shifted all domain tag/ref generation into a single file.

commit 8e68414a3dc767dbeb589172e82dfbd5339ab569
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 22 15:03:13 2011 +0100

    Adding 'mentioned' generation.

    This is used to generate frame conditions which can exclude
    certain objects (ie, the mentioned ones).

commit cbc6b82f4a00314b3ae76d7eb513c37d31d1dca3
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 22 15:01:57 2011 +0100

    Domain generation produces general yices file.

    The general yices file pulls together all the type definitions
    and wraps them.

commit 489bffafddda0f22277737b5f3c6130d23371d10
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 22 11:07:03 2011 +0100

    Fixing shared feature global implementation.

commit c352581a87c596ecd3f9ae0ccb1754a143048094
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 22 10:30:22 2011 +0100

    Adding a mentioned query.

    The mentioned query pulls out all variables that are mentioned
    in an expressionn.

commit 741858863ce9538bfa7ededbec6de7f0d1cdb039
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 21 14:57:49 2011 +0100

    Generation action for a single class.

commit 65afc9d130897a9a45c9b595c7c232943389b94c
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 21 14:57:24 2011 +0100

    Suppliers processing args, tags, refs-wrapping.

commit e14e2f93b3306b914b6a4615883f98703a08b43e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 21 13:39:21 2011 +0100

    Reorganizing s-expr util, adding supplier processing.

    Some changing around of where the utility functions for s-exprs live.
    Also introducing generation of the module to gather supplier data together
    so more than one class can be used for planning.

commit 1ca7cb0bcb4343886af2da501da77e017c64f5a6
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 21 13:11:23 2011 +0100

    Yices generation involving all suppliers.

commit c68c206102d10e3a8b7ae105f64d2d46ca894075
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 21 10:14:53 2011 +0100

    Organizing a few features into sections.

commit 78c4d33f536acea3f9db88c5a234e89a54bce257
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 21 09:39:49 2011 +0100

    using the prefixed_name function

commit 8c3f0e2e1966b78bfd11d438ac0d58434774680e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Mar 18 13:13:07 2011 +0100

    Move some functions to standalone sexpr library.

commit 208f0a2f515e4d0309a36c718283db00dbbd6d3f
Merge: e0e4f9c 09adbc3
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Mar 18 11:19:56 2011 +0100

    Merge branch 'master' into simpler_ssa

commit e0e4f9c76abfa98dca19ff59ec5375358dfd8a45
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Mar 18 10:35:47 2011 +0100

    Adding equality generation sexpr utility.

commit e2baf8b05b761e804adf6a3d474124ac0638f10b
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 17:07:04 2011 +0100

    Removing unused classes from old instrumentation.

commit fe15c217505ce0142ff6c8d336b67477b259dee9
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 16:03:29 2011 +0100

    Inserting call to rely_plan in generated code.

commit 10c800811f37772228271048916dd8e0d0002752
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 14:40:11 2011 +0100

    Change name to 'instrument', more descriptive.

commit cf01280d30dccd8a106c34b25bf44a4343ccee6f
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 14:25:41 2011 +0100

    Process ifs and assignments in ssa printer.

commit 07f2c5aa00ba88178cd12b003dd482ae691732e6
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 14:25:18 2011 +0100

    Fix pre-conditions of attributes as 'true'.

commit aff4e839685c3a6d05831e03a67a8be3d647316e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 11:24:39 2011 +0100

    Fixing double-output of precondition, cleanups.

    Unnecessary variables related to the old approach have been removed.

commit 7fe990976da7e3dd33359942683045422b1b863b
Merge: 9134fe8 f8c33db
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 10:31:35 2011 +0100

    Merge branch 'master' into simpler_ssa

    Conflicts:
    	Src/Eiffel/Ace/ec.ecf

commit 9134fe898345e50a89c0df31978eb028394813b1
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 10:29:16 2011 +0100

    No need to save shared feature_i.

commit 63b2523cfb7bfb55c4e4862546be6b3912e1699d
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Mar 17 10:28:51 2011 +0100

    Detabifying feature printer.

commit b476086f08189f30ea4e5c860cd12a71c0033b9f
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 16:41:26 2011 +0100

    Preconditions can now be instantiated properly.

    Before, the expression generation worked only for non-instantiated
    arguments, but now those can be mapped to particular expressions
    (actual arguments).

commit 6e50f618f2aa6e75c08920aee749c7c8a549acbe
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 15:15:54 2011 +0100

    Removing unused local.

commit fb23cc38217f51912a6e54f6dd31c74cfcce91b0
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 14:57:51 2011 +0100

    untabifying

commit 03b87ee48601bcba1fe6058c2efd430a0444a5a6
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 14:57:21 2011 +0100

    Formatting update.

commit 2889d6e2090a29337ec412cfb5c4a33085d6e130
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 14:46:38 2011 +0100

    Removing the usage of the ARRAY.

    Replaced this with an ARRAYED_LIST which allows for much cleaner code.

commit 653b52fb64238bc2f57833aacd58314b882503c6
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 14:36:40 2011 +0100

    Removing additionally unneeded checks.

commit 0c686c4dd832a684f0fe22fd153c9da254332abc
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 14:33:48 2011 +0100

    Removing  initial Result+, result is initially Void.

commit 6b0cb7e50381e08a8b2410a57c67a173fcfe51a1
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 14:33:03 2011 +0100

    Removing void-branching code, target is always attached.

commit 3cfd6c06174fcbb7e0c4ee3225cf6eb6edf431cd
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 11:18:41 2011 +0100

    Further removal of old replacement scheme.

commit e16fabaa720b123ef2cacdcd341df9e45c3694d5
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 11:07:50 2011 +0100

    Removing printed_locals flag.

commit eef58a1ba15af9623c5b471784414172b6751839
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 11:06:12 2011 +0100

    Continuing to clean out old instrumentation.

    Locals are no longer added, for instance.

commit 01c4bdb57054d38960d2a16f029c2956b4d21398
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 10:59:42 2011 +0100

    Reworking the expression tree slightly.

    The tree now demands that nested calls have a non-void target.
    To fill this in a new node has been created to take the place of
    Current, (we call it "this" to avoid name overloading).

    Some old replacement code is being stripped away as well.

commit fe84c1867496c8cb5dc2409f9074c955862c2566
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 10:06:13 2011 +0100

    Adding creation precondition, simplifying all_pre_conds.

    The precondition on the creation procedure should enforce that the
    variable is not a feature, but a true variable (formal argument or local).

    The all_pre_conditions now returns an empty list.

commit ed8dda1920ec3f76afd6bc5e86dba8e7f6491204
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 15 10:01:44 2011 +0100

    Formatting update.

commit 5cb8e526d349a2eb301ea9501719413cd184c7d9
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 14 17:38:20 2011 +0100

    Formatting update.

commit 96dd74ee71edd33eeeb739b0be730e6e7d736e5d
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 14 17:27:13 2011 +0100

    First step towards simpler instrumentation.

    Preconditions are extracted from syntax trees and turned into a list
    of s-expressions.

commit 714969891d55318fa649eab162c3bf44df01c38c
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 14 16:04:50 2011 +0100

    Detabifying ssaifier.e.

commit 696b9cc0eaf2ed4be5a8c3a0791c760ed68f44ff
Merge: ad2b9bf da9948f
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Mar 14 14:16:03 2011 +0100

    Merge branch 'master' into demonic_testing

commit ad2b9bf0a12077a1be23148017e78b1b5467231b
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Mar 9 09:47:01 2011 +0100

    Reworking the index lambda.

commit 62418173d5c0397b272eff1f6945774bebd2d54a
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Mar 9 09:46:15 2011 +0100

    Fixing boolean output, lower-case only.

commit f9720d1cf03d10dcb579813e5c97003fc729e964
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Mar 9 09:44:56 2011 +0100

    Fixing once would should have been a 'do'.

commit b65149b1266994dfad4dddb07b37054c4171dad2
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Mar 2 13:28:10 2011 +0100

    Generating frame only after functions and attributes.

commit 0351223afe87e17a71bf1916ea9855298d7f0d5b
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Mar 2 13:26:56 2011 +0100

    Changing delcaration generation to omit parentheses.

commit 636bcbf817c554aba36ea8601f91cd40374c2ab9
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Mar 2 12:39:03 2011 +0100

    Using BOOL_AS.value now to get literal boolean.

commit 710d022f848e436ac2497ef6421fcc526289ca53
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Mar 2 11:18:00 2011 +0100

    Process `Result=' style funcs, fix index in procedures.

    Adding a few utility function to generate the indexed-lambda,
    and changing the name of the attribute_name to a more general
    prefixed_name as it will work on any type and string.

commit d2083f406327864aa8dbbb04922ffaeb02a32249
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 17:02:39 2011 +0100

    Add stub generating lambda for Eiffel functions.

commit f1e71025d9675b50b161742d4bd7dbb9113b6eb3
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 17:00:22 2011 +0100

    Updating variable name in mk_lambda.

commit 0f473c2efd459fc56a10f54b0cd2f29579ce6b7e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:44:50 2011 +0100

    Formatting update.

commit 39389ea845c2f78b00cf777edb6252138a66d422
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:35:35 2011 +0100

    Setting the shared feature_i from the domain generation.

commit 3902c5cd645e9675f671c2fe90b0e88fcf96facc
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:34:52 2011 +0100

    Nested features now use `type.

    Also added a new feature which gets the type of the target, as it can be
    Void is must be treated specially.

commit 8f674e47fedfb75a508eda5f0b7d912fa01f99bc
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:34:29 2011 +0100

    SSA_EXPR_VAR now uses the `type' feature.

commit 536f7da8339b819ab03f74b6c8a7cbce8f071c2c
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:33:53 2011 +0100

    Overriding new type feature when the operator is `old'

commit c102bf406dfcb7fc2936528a74ee65e2e49e48f7
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:31:21 2011 +0100

    Adding a `type' feature to SSA_EXPR.

commit 99742e1f60eeb079f3404d8b8841bc6748a18e62
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:29:58 2011 +0100

    DOMAINIFIER now uses SSA_SHARED

commit 1633341fe4a563f5791045a8d67ae4a0c8790c64
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:29:24 2011 +0100

    Using a CELL internally in SSA_SHARED.

commit d01d1bcde8a2484720365620e5c6bca61633091d
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 16:29:05 2011 +0100

    Removing debugging print.

commit 1c48dd9ec5e1a028a235b3373b8201ec261a9079
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 12:01:10 2011 +0100

    Fixing indentation: spaces -> tabs.

commit b1bd6eb0defbe50865a15d645247bc0a46c7582e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 10:09:53 2011 +0100

    Adding conversion function from classes to names.

    This makes it possible to remove generic arguments from types. Any function
    which was generating its own prefix based on classes now uses this.

commit e1bc84fcb27df0994328e88328499c255f0047a5
Merge: b0b1adc 950b7bb
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 09:20:09 2011 +0100

    Merge branch 'master' into demonic_testing

commit b0b1adc0575cb1f684b50086800709ecfe9aec21
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 09:18:51 2011 +0100

    Adding frame generation, name conversion utilities.

    The name conversion utilities are to try to combat some fragility in the
    way names are generated.

commit 09fb2f9c81fdd6886dac271905071f54111dc94e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Mar 1 08:46:10 2011 +0100

    Formatting changes.

commit d1a2b47c6ef769e7769fb251db4c5842be3106b0
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 24 11:20:04 2011 +0100

    Off by one in "this"-prepended arguments of a nested call.

commit 687e138f4f9e6fa68953e33819bb5bae0255edcf
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 24 11:13:28 2011 +0100

    Ignore class invariant processing.

commit 79bd76adc5ce5f9359130aa7b42645c89eaeb0b0
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 24 11:12:05 2011 +0100

    Check-false -> print TODO for converting functions.

commit 9432da19de72af94a98ce802d25e2eba30b19d16
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 14:55:55 2011 +0100

    Cleaning up small items.

commit 33383cf11f39b88bd052fa2ef8542736456fe63d
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 13:52:11 2011 +0100

    File output using domain_string from the yices domain class.

commit 4d8bbb64dfa9a2c8d0629231f6b4bbeda678c75b
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 13:51:22 2011 +0100

    New feature to convert class to yices string.

commit b78a1c793d55aa6a345ab5da21114c5f0db0df09
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 13:45:14 2011 +0100

    Output the domain now into a file, rather than stdio.

commit e085264a05d1ed0c728975c76c6db85c89d948b2
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 13:04:50 2011 +0100

    Generate action tags.

commit b4813e6fd2cae494c13b7ea1c8e397e7ccdf4b72
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 12:57:18 2011 +0100

    Adding define_type and mk_scalar functions.

    These are now used to reformulate the temp objects for a given class.

commit 1114ae6829055d6bef76765c12dedfac101e7dd3
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 11:18:06 2011 +0100

    Using the mk_and utility function.

commit 38b7172c333caee417d7b0909023fa32af5b7e69
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 10:15:36 2011 +0100

    Updating formating.

commit 6d0711467d8c07ef004e6635849fc0ea24864488
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 09:49:32 2011 +0100

    Using mk_list in ssa nested expressions.

commit b99e099badcb342bd8074ffd276cc5bbb7e24b3b
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 09:48:55 2011 +0100

    Now using mk_list in yices domain generation.

commit 4778c96afb90b4d6490d81425211c669f6448c23
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 09:48:01 2011 +0100

    Using now mk_list in yices utilities.

commit d05e3c52f11490d0dbcb8bb9f9d3bc1b3e198001
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 09:47:03 2011 +0100

    Updating declaration generation.

    Removing the outer parenthesis to be more in line with what YICES uses for syntax.
    The other may have worked, but this seems more idiomatic from the documentation of YICES.

commit 50960d2a174d04fa4593de793a07eaa0a4b60a9b
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Wed Feb 23 09:44:42 2011 +0100

    Adding mk_list s-expression utility.

commit a1ff3efac1a10d5b9af03bc788993670944af652
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 17:19:06 2011 +0100

    Refactored ssa_yices_domain.

    The common yices functionality now lives in a utility class,  allowing
    the domain construction class to be much smaller and cleaner.

commit 49a99adaec60dcdf5c3d9687031aa2eaf9cc53fb
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 17:18:47 2011 +0100

    Domainifier now prints out the yices domain.

    This is just a temporary thing so it can be seen easily while worked on. The output
    was moved here so that the ssa-yices-domain class could be cleaned up.

commit 30107513bc23ef6d416390b54598654aec9cf727
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 16:23:43 2011 +0100

    Changing static type of empty_list to ARRAYED_LIST.

commit 74e9e68a22e699e5426c2aed977cd305b80056dc
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 16:21:50 2011 +0100

    Domain now returns a single sexpr.

    Debugging printing of the class domain has now been removed as well.

commit 29f713d6a1991a1089b893f3012b2d141bdea19d
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:52:00 2011 +0100

    Removing obsolete feature call.

commit 113b7c0a53fd2dc35b7cfc03e990d27492a8c0ee
Merge: 1b8408f 7e32534
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:47:37 2011 +0100

    Merge branch 'master' into demonic_testing

commit 1b8408f7610005486cb4af9087d1183db94f18b6
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:46:33 2011 +0100

    Fixing function calls with indices.

    Now the indexes are used to form the function call, before
    they were omitted.

commit d5bfa513693ce6f5f8559cba4dbe912bfdd76f0e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:45:06 2011 +0100

    Enhancing expression fixer.

    The fixer now incorporates the argument list so it can distinguish
    formal arguments from unqualified calls.

    Related updates have been made in the clients.

commit 29dd4d39ba0cb26e983940ad2a61f59ea77e6414
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:18:47 2011 +0100

    Untabing expr_fixer.

commit ac4e3297dc87f00cc3d8c537810e780fa5b5d1ba
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:09:37 2011 +0100

    Fixing runtime crashes and some output bugs.

commit e5fa7cd116ff3677bbe243fc218743468f213ccf
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:09:19 2011 +0100

    Adding invariants to class descr.

commit 7dfdc5255b77d7fa65093bd39ecc48feaa82df8b
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:07:50 2011 +0100

    Inserting calls to yices domain conversion.

commit 15233ddf4442d3266b929e98c0c4bf6b4353e762
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:07:22 2011 +0100

    Including invariants in declarations.

commit c650764419923c783932c4968f493235a2078a0e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 22 14:06:59 2011 +0100

    Initializing arguments list in feature descr.

commit 72c7823cf444542ba5be8ea92a60bac26781a106
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Feb 21 17:07:43 2011 +0100

    Class-to-yices pre-post condition conversion.

commit 67f3562748e06864e6dd77486eb196a27c72de37
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Feb 21 16:37:28 2011 +0100

    Add function to translate args to types.

    The argument declarations are taken in combination with the target type
    to generate a type declaration that includes all names/types.

commit a02dc912ac0045f7a080e6a72cb953a9bf02772b
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Feb 21 15:36:54 2011 +0100

    Cleaning, adding some skeleton implementations.

commit 6a6a39d01034c10a216c729e8e901508a3265679
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Feb 21 15:36:17 2011 +0100

    Updating ssa expressions to convert to sexprs.

commit 4420a50c305b2c0614b8e940de1556d626b0403d
Merge: 9d12b43 c5083f0
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Feb 21 14:31:45 2011 +0100

    Merge branch 'master' into demonic_testing

commit 9d12b4346ce11faa93435755f6ba4e76f86047b7
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Mon Feb 21 14:30:20 2011 +0100

    Updates to yices domain conversion, sexpr utils.

    The class description is now based on type, not name. Suitable updates
    have been made to the higher-level classes to use this convention.

commit ad3fba02ba8446fb4336661d020c63520ccb9604
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 18:05:42 2011 +0100

    Adding utility and ecf for sexprs.

commit a1f146582e0e17339aa6f31979a2f1156d503365
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 18:04:39 2011 +0100

    Skeleton of description to domain transformation.

commit 408bde81637f1a46b99262150d131421c563671f
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 18:04:04 2011 +0100

    Adding yices domain class to class transformation.

commit 2dda218349ab223e50f0b73dcbdf866f4d9e6a42
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 18:01:07 2011 +0100

    Fixing for new sexpr class.

commit c37a4b8f2b836e7e9941b56819c79141db5399ab
Merge: 649bd19 acfe266
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 16:45:57 2011 +0100

    Merge branch 'master' into demonic_testing

    Conflicts:
    	Src/Eiffel/Ace/ec.ecf

commit 649bd197f2f75490067134a38358db17dfc4f139
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 16:36:38 2011 +0100

    Converting to use sexpr library.

    This change is part of the move to yices as a planning back-end.

commit ba248b948822f000cd52eb4961d041d36123ecf4
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 15:20:55 2011 +0100

    Fixing typo in sexpr_const

commit 3ceda65879948d23afbbab3337f591c431e60cdd
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 13:34:48 2011 +0100

    Removing unneeded expression types.

commit 0351ff1db4cb5b6d76eb4a736a64b0a942346289
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 13:33:49 2011 +0100

    Renaming expression classes to include sexpr.

commit d387ca45a7e6bac323a9fddcc4ca1a2abb90a37d
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Fri Feb 18 13:30:29 2011 +0100

    Moving sexprs into their own module.

commit 8448354baea08c1fe28c90c94049608f40822a21
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 17 17:16:51 2011 +0100

    Adding yices conversion class.

commit 28b44597c8c9364f3cac4f5f0f8c1bce90f16af6
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 17 17:16:23 2011 +0100

    Fixing small compile errors.

commit 25a712020d6944c06fc2f40ae03dffd7d38c2c1a
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 17 17:16:11 2011 +0100

    Fixing typo.

commit 412f1b097bda73c95867ed5ae72401ec3424d21a
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 17 16:28:29 2011 +0100

    Adding arguments to feature description.

commit 2f5d62155e627d3e07aa5f0ce20a15ffaf9cdf8a
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 17 16:27:07 2011 +0100

    Yices conversion now generates *_desc classes.

commit b89a564b2640ee6a303abc58ff3ab4c0086b727e
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 17 14:15:43 2011 +0100

    Adding classes for describing classes and features.

commit bc072f2c0e2f0555d86413c5d0652d74764e4371
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 17 13:57:14 2011 +0100

    Copy of class_to_domain for SMT encoding.

commit 6e48deecd7d38e3d1f308c49c83c7f38b57d03b8
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Thu Feb 17 13:50:20 2011 +0100

    Renaming inconsistent class/filenamed pre_to_adl.

commit bf9db246b96cd870f05fa090b9492ba17d7444a9
Merge: d7a8fe8 2f5b47d
Author: Scott West <scott.west@inf.ethz.ch>
Date:   Tue Feb 15 16:22:56 2011 +0100

    Merge branch 'master' into demonic_testing

commit d7a8fe808398a14258f4897a9841c863d8bc04e1
Author: S <saynte@gmail.com>
Date:   Mon Feb 7 00:07:37 2011 +0100

    Adding back inclusion of target.

    This broke the previous instrumentation.

commit e51212f7fb75e6028d8878451ef197be359c62de
Author: S <saynte@gmail.com>
Date:   Sun Feb 6 22:38:56 2011 +0100

    Adding gitignore.

commit 89a8ff586c00d0ce45c71fe67d58dd6ef5d46106
Author: S <saynte@gmail.com>
Date:   Sun Feb 6 22:17:41 2011 +0100

    Removing parameter serialization.

    This is now taken care of by the arguments, due to the replacement
    in the rely condition we can do this.

commit dde91511b497ba5f78307e73cbec5790dbf418b5
Author: S <saynte@gmail.com>
Date:   Sun Feb 6 22:15:48 2011 +0100

    Track assignments with a parameter as source.

    When we have an assignment from a parameter, we store it so we can
    update rely-conditions with it.

commit e37f2aa288f2b7a89c59cdff5766cd3018ce4049
Author: scott <scott@scott-desktop.(none)>
Date:   Sun Feb 6 18:21:15 2011 +0100

    Initial commit of demonic testing branch.

Revision 86265 - (view) (annotate) - [select for diffs]
Modified Fri Apr 15 12:40:05 2011 UTC (8 years, 8 months ago) by jasonw
File length: 2768 byte(s)
Copied from: trunk/.gitignore revision 86264
Diff to previous 86255
<<Merged from trunk#86264.>>

Revision 86255 - (view) (annotate) - [select for diffs]
Modified Thu Apr 14 13:44:31 2011 UTC (8 years, 8 months ago) by jfiat
Original Path: trunk/.gitignore
File length: 2768 byte(s)
Diff to previous 86253
more .gitignore content

Revision 86253 - (view) (annotate) - [select for diffs]
Modified Thu Apr 14 13:22:31 2011 UTC (8 years, 8 months ago) by jfiat
Original Path: trunk/.gitignore
File length: 2671 byte(s)
Diff to previous 86251
updated file due to typo

Revision 86251 - (view) (annotate) - [select for diffs]
Added Thu Apr 14 13:00:47 2011 UTC (8 years, 8 months ago) by jfiat
Original Path: trunk/.gitignore
File length: 2756 byte(s)
Added some files to ease the use of git-svn on this subversion repository
This has no impact on EiffelStudio source code.

This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.23