/[eiffelstudio]/branches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_helper.e
ViewVC logotype

Log of /branches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_helper.e

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 94771 - (view) (annotate) - [select for diffs]
Modified Thu Apr 3 12:37:44 2014 UTC (5 years, 6 months ago) by polikarn
File length: 26804 byte(s)
Diff to previous 94603
Bugfix: redefinitions now taken into account when calculating replaced model queries.

Revision 94603 - (view) (annotate) - [select for diffs]
Modified Fri Mar 14 18:21:48 2014 UTC (5 years, 7 months ago) by polikarn
File length: 26245 byte(s)
Diff to previous 94492
Removed global_public (super slow) and added annotations as a consequence; reseting type/var counters after every verification; changed EB2 specs to verify with the sound invariant frame axiom.

Revision 94492 - (view) (annotate) - [select for diffs]
Modified Sat Feb 22 17:22:35 2014 UTC (5 years, 7 months ago) by polikarn
File length: 26139 byte(s)
Diff to previous 94461
Verified CELL_CURSOR. Minor bugfix. Renamed ghost index.

Revision 94461 - (view) (annotate) - [select for diffs]
Modified Fri Feb 21 15:39:42 2014 UTC (5 years, 8 months ago) by polikarn
File length: 26110 byte(s)
Diff to previous 94427
Fixes in model replacement mechanism. Verified LIST (except remove, remove_all). Cleaned up base2.

Revision 94427 - (view) (annotate) - [select for diffs]
Modified Thu Feb 20 19:18:16 2014 UTC (5 years, 8 months ago) by polikarn
File length: 25237 byte(s)
Diff to previous 94356
Closing abstract frames under model replacements; checking that replacing models are new.

Revision 94356 - (view) (annotate) - [select for diffs]
Modified Tue Feb 18 16:56:47 2014 UTC (5 years, 8 months ago) by julian
File length: 20746 byte(s)
Diff to previous 94334
AutoProof: Improve translation speed by caching map features.
AutoProof: Improve translation speed by only compiling on workbench changes.

Revision 94334 - (view) (annotate) - [select for diffs]
Modified Sun Feb 16 16:53:58 2014 UTC (5 years, 8 months ago) by polikarn
File length: 20327 byte(s)
Diff to previous 94249
Implemented update guards.

Revision 94249 - (view) (annotate) - [select for diffs]
Modified Mon Feb 10 18:53:59 2014 UTC (5 years, 8 months ago) by polikarn
File length: 20154 byte(s)
Diff to previous 94244
Fixed some typing issues.

Revision 94244 - (view) (annotate) - [select for diffs]
Modified Sun Feb 9 18:58:57 2014 UTC (5 years, 8 months ago) by polikarn
File length: 19957 byte(s)
Diff to previous 94233
New approach to abstract framing: model queries are inherited. Big typing refactoring: uniform conversion and type-safe conversion to class types all over the place.

Revision 94233 - (view) (annotate) - [select for diffs]
Modified Fri Feb 7 13:45:10 2014 UTC (5 years, 8 months ago) by polikarn
File length: 18538 byte(s)
Diff to previous 94212
Minor bugfix and refactoring.

Revision 94212 - (view) (annotate) - [select for diffs]
Modified Thu Feb 6 14:05:02 2014 UTC (5 years, 8 months ago) by polikarn
File length: 18534 byte(s)
Diff to previous 94194
Freshness. Changed conditions for modifying observers. First 3 classes of EB2 with models.

Revision 94194 - (view) (annotate) - [select for diffs]
Modified Wed Feb 5 18:28:39 2014 UTC (5 years, 8 months ago) by polikarn
File length: 18431 byte(s)
Diff to previous 94155
Handling model fields in frames.

Revision 94155 - (view) (annotate) - [select for diffs]
Modified Sat Feb 1 16:06:43 2014 UTC (5 years, 8 months ago) by polikarn
File length: 17417 byte(s)
Diff to previous 94075
A3 checks.

Revision 94075 - (view) (annotate) - [select for diffs]
Modified Wed Jan 22 18:08:57 2014 UTC (5 years, 9 months ago) by polikarn
File length: 17385 byte(s)
Diff to previous 94058
Added read checks.

Revision 94058 - (view) (annotate) - [select for diffs]
Modified Sat Jan 18 16:45:31 2014 UTC (5 years, 9 months ago) by polikarn
File length: 17163 byte(s)
Diff to previous 94027
Added free invariants to logical types; tests for bags; bugfixes.

Revision 94027 - (view) (annotate) - [select for diffs]
Modified Thu Jan 16 12:28:06 2014 UTC (5 years, 9 months ago) by polikarn
File length: 16815 byte(s)
Diff to previous 94026
Mapping termination metric through <= alias.

Revision 94026 - (view) (annotate) - [select for diffs]
Modified Thu Jan 16 12:03:20 2014 UTC (5 years, 9 months ago) by polikarn
File length: 16792 byte(s)
Diff to previous 93981
Mapping logical equality through is_equal.

Revision 93981 - (view) (annotate) - [select for diffs]
Modified Tue Jan 14 13:18:00 2014 UTC (5 years, 9 months ago) by polikarn
File length: 15470 byte(s)
Diff to previous 93969
Generic mechanism to map logical classes to Boogie map types.

Revision 93969 - (view) (annotate) - [select for diffs]
Modified Mon Jan 13 12:52:16 2014 UTC (5 years, 9 months ago) by polikarn
File length: 14923 byte(s)
Diff to previous 93962
Improved error reporting, bugfix in IV_TYPES.

Revision 93962 - (view) (annotate) - [select for diffs]
Modified Sun Jan 12 19:42:00 2014 UTC (5 years, 9 months ago) by polikarn
File length: 14424 byte(s)
Diff to previous 93942
Big refactoring: made the IV_TYPE hierarchy more flexible; logical types are not hardcoded, but defined through special note clauses.

Revision 93942 - (view) (annotate) - [select for diffs]
Modified Thu Jan 9 09:53:26 2014 UTC (5 years, 9 months ago) by polikarn
File length: 14187 byte(s)
Diff to previous 93812
Moved set and sequence theories to MML. Using note 'theory' to include Boogie files.

Revision 93812 - (view) (annotate) - [select for diffs]
Modified Thu Dec 26 18:08:04 2013 UTC (5 years, 9 months ago) by polikarn
File length: 13919 byte(s)
Diff to previous 93790
More general loop variants: multiple components, different types, checked by default, variant inference. Refactored loop processing into multiple subroutines.

Revision 93790 - (view) (annotate) - [select for diffs]
Modified Mon Dec 23 16:51:45 2013 UTC (5 years, 10 months ago) by polikarn
File length: 13137 byte(s)
Diff to previous 93735
Added Eiffel equivalents for writable checks and in_domain; added line numbers to validity errors; bugfix: adding type when doing class check for an empty class.

Revision 93735 - (view) (annotate) - [select for diffs]
Modified Mon Dec 16 13:19:17 2013 UTC (5 years, 10 months ago) by julian
File length: 13003 byte(s)
Diff to previous 93713
AutoProof: fixed typo.

Revision 93713 - (view) (annotate) - [select for diffs]
Modified Fri Dec 13 16:24:13 2013 UTC (5 years, 10 months ago) by polikarn
File length: 12651 byte(s)
Diff to previous 93640
Removed some unnecessary checks, added semantic warnings.

Revision 93640 - (view) (annotate) - [select for diffs]
Modified Fri Dec 6 15:49:56 2013 UTC (5 years, 10 months ago) by julian
File length: 12025 byte(s)
Diff to previous 93597
AutoProof: finished refactoring of error display.

Revision 93597 - (view) (annotate) - [select for diffs]
Modified Tue Dec 3 00:48:44 2013 UTC (5 years, 10 months ago) by julian
File length: 12074 byte(s)
Diff to previous 93572
AutoProof: special translation for lemma and functional

Revision 93572 - (view) (annotate) - [select for diffs]
Modified Thu Nov 28 16:42:09 2013 UTC (5 years, 10 months ago) by julian
File length: 11666 byte(s)
Diff to previous 93569
AutoProof: added validity check for partial invariants.

Revision 93569 - (view) (annotate) - [select for diffs]
Modified Thu Nov 28 09:17:16 2013 UTC (5 years, 10 months ago) by julian
File length: 11012 byte(s)
Diff to previous 93532
AutoProof: added support for comparing sets and sequences

Revision 93532 - (view) (annotate) - [select for diffs]
Modified Mon Nov 25 22:25:26 2013 UTC (5 years, 10 months ago) by polikarn
File length: 10544 byte(s)
Diff to previous 93523
Relaxed defaults and adjusted tests accordingly. Built-in function inv.

Revision 93523 - (view) (annotate) - [select for diffs]
Modified Sat Nov 23 07:32:23 2013 UTC (5 years, 11 months ago) by julian
File length: 10404 byte(s)
Diff to previous 93302
AutoProof: added better feedback for unsupported code.

Revision 93302 - (view) (annotate) - [select for diffs]
Modified Mon Nov 11 07:04:29 2013 UTC (5 years, 11 months ago) by julian
File length: 9927 byte(s)
Diff to previous 93272
AutoProof: added defaults in invariant clause for ownership.

Revision 93272 - (view) (annotate) - [select for diffs]
Modified Fri Nov 8 16:50:37 2013 UTC (5 years, 11 months ago) by julian
File length: 10061 byte(s)
Diff to previous 93245
AutoProof: added defaults for ownership methodology

Revision 93245 - (view) (annotate) - [select for diffs]
Modified Thu Nov 7 16:44:12 2013 UTC (5 years, 11 months ago) by julian
File length: 9001 byte(s)
Diff to previous 93152
AutoProof: continued ownership implementation.

Revision 93152 - (view) (annotate) - [select for diffs]
Modified Mon Oct 21 15:20:06 2013 UTC (6 years ago) by julian
File length: 8834 byte(s)
Diff to previous 91221
AutoProof: Added infrastructure to translate ghost state.

Revision 91221 - (view) (annotate) - [select for diffs]
Modified Tue Feb 12 16:58:15 2013 UTC (6 years, 8 months ago) by julian
File length: 7928 byte(s)
Diff to previous 88710
AutoProof: update to Array translation.

Revision 88710 - (view) (annotate) - [select for diffs]
Added Thu May 10 14:58:31 2012 UTC (7 years, 5 months ago) by julian
File length: 7930 byte(s)
Added new AutoProof version with translation to intermediate verification AST for translation to Boogie.


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