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

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

Parent Directory Parent Directory | Revision Log Revision Log


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

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: 7850 byte(s)
Diff to previous 93349
AutoProof: special translation for lemma and functional

Revision 93349 - (view) (annotate) - [select for diffs]
Modified Wed Nov 13 17:15:59 2013 UTC (5 years, 11 months ago) by julian
File length: 9227 byte(s)
Diff to previous 93211
AutoProof: added predicates for partial invariants

Revision 93211 - (view) (annotate) - [select for diffs]
Modified Tue Nov 5 23:10:23 2013 UTC (5 years, 11 months ago) by julian
File length: 8971 byte(s)
Diff to previous 93175
AutoProof: continued ownership implementation.

Revision 93175 - (view) (annotate) - [select for diffs]
Modified Mon Oct 28 16:27:38 2013 UTC (5 years, 11 months ago) by julian
File length: 8669 byte(s)
Diff to previous 93163
AutoProof: initial refactoring for routine translators.
AutoProof: added two examples.

Revision 93163 - (view) (annotate) - [select for diffs]
Modified Wed Oct 23 00:33:57 2013 UTC (5 years, 11 months ago) by julian
File length: 8667 byte(s)
Diff to previous 93152
AutoProof: added translation for ghost attributes.
AutoProof: cleanup.

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

Revision 93127 - (view) (annotate) - [select for diffs]
Modified Wed Oct 16 15:19:13 2013 UTC (6 years ago) by julian
File length: 6194 byte(s)
Diff to previous 92762
AutoProof: added more Array functions to theory.
AutoProof: always generate and use a specific Boogie file in EIFGEN directory.
AutoProof: update to testing infrastructure.

Revision 92762 - (view) (annotate) - [select for diffs]
Modified Mon Jul 1 16:00:14 2013 UTC (6 years, 3 months ago) by polikarn
File length: 6126 byte(s)
Diff to previous 92742
Added some tests for MML_SET features

Revision 92742 - (view) (annotate) - [select for diffs]
Modified Wed Jun 26 17:45:24 2013 UTC (6 years, 3 months ago) by polikarn
File length: 6064 byte(s)
Diff to previous 91213
Calling creation version of a procedure from creation expressions; generating creation procedure from default_create; translating MML_SET.is_disjoint.

Revision 91213 - (view) (annotate) - [select for diffs]
Modified Mon Feb 11 15:42:55 2013 UTC (6 years, 8 months ago) by julian
File length: 5741 byte(s)
Diff to previous 91096
AutoProof: Continued ownership translation.


Revision 91096 - (view) (annotate) - [select for diffs]
Modified Thu Jan 31 16:28:35 2013 UTC (6 years, 8 months ago) by julian
File length: 5683 byte(s)
Diff to previous 88710
Separate Boogie translation for creation routines.
Added incomplete ownership 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: 5260 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