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

Log of /branches/eth/eve/Src/framework/eiffel2boogie/translation/custom/e2b_custom_ownership_handler.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: 8837 byte(s)
Diff to previous 93579
AutoProof: special translation for lemma and functional

Revision 93579 - (view) (annotate) - [select for diffs]
Modified Thu Nov 28 19:46:33 2013 UTC (5 years, 10 months ago) by polikarn
File length: 8843 byte(s)
Diff to previous 93572
Fixed contracts in other examples. Made closed a real attribute. Better translation of built-in attributes in modify field.

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: 9511 byte(s)
Diff to previous 93532
AutoProof: added validity check for partial invariants.

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: 8065 byte(s)
Diff to previous 93525
Relaxed defaults and adjusted tests accordingly. Built-in function inv.

Revision 93525 - (view) (annotate) - [select for diffs]
Modified Mon Nov 25 07:31:05 2013 UTC (5 years, 10 months ago) by julian
File length: 7792 byte(s)
Diff to previous 93523
AutoProof: started with PIP example

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

Revision 93405 - (view) (annotate) - [select for diffs]
Modified Fri Nov 15 21:07:40 2013 UTC (5 years, 11 months ago) by julian
File length: 7338 byte(s)
Diff to previous 93378
AutoProof: continued ownership implementation.


Revision 93378 - (view) (annotate) - [select for diffs]
Modified Thu Nov 14 15:57:08 2013 UTC (5 years, 11 months ago) by julian
File length: 7376 byte(s)
Diff to previous 93349
AutoProof: continued ownership implementation.


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: 7377 byte(s)
Diff to previous 93346
AutoProof: added predicates for partial invariants

Revision 93346 - (view) (annotate) - [select for diffs]
Modified Wed Nov 13 08:05:21 2013 UTC (5 years, 11 months ago) by julian
File length: 6076 byte(s)
Diff to previous 93215
AutoProof: added composite example.

Revision 93215 - (view) (annotate) - [select for diffs]
Modified Wed Nov 6 15:55:58 2013 UTC (5 years, 11 months ago) by julian
File length: 5683 byte(s)
Diff to previous 93211
AutoProof: continued ownership implementation.

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: 5459 byte(s)
Diff to previous 93186
AutoProof: continued ownership implementation.

Revision 93186 - (view) (annotate) - [select for diffs]
Modified Wed Oct 30 16:08:59 2013 UTC (5 years, 11 months ago) by julian
File length: 5397 byte(s)
Diff to previous 92868
AutoProof: continue on ownership implementation.

Revision 92868 - (view) (annotate) - [select for diffs]
Modified Thu Aug 8 14:27:47 2013 UTC (6 years, 2 months ago) by polikarn
File length: 5350 byte(s)
Diff to previous 92756
Meningful tags for ownership checks. Adapted to the new Boogie output format. Handling precondition violations of fake procedures (like update_heap). Ownership checks for heap assignents. Dynamic type of Current is known.

Revision 92756 - (view) (annotate) - [select for diffs]
Modified Fri Jun 28 17:43:08 2013 UTC (6 years, 3 months ago) by polikarn
File length: 4988 byte(s)
Diff to previous 92732
Made MML_SET generic; translating the rest of MML_SET features; properly translating alias binary operators

Revision 92732 - (view) (annotate) - [select for diffs]
Modified Mon Jun 24 15:19:19 2013 UTC (6 years, 3 months ago) by polikarn
File length: 4726 byte(s)
Diff to previous 92731
Generalized OWNERSHIP_SET to MML_SET, added its own handler with translation for has.

Revision 92731 - (view) (annotate) - [select for diffs]
Modified Mon Jun 24 13:23:44 2013 UTC (6 years, 3 months ago) by julian
File length: 4718 byte(s)
Diff to previous 92724
added GUI option to enable ownership.

Revision 92724 - (view) (annotate) - [select for diffs]
Modified Fri Jun 21 11:44:49 2013 UTC (6 years, 3 months ago) by polikarn
File length: 4655 byte(s)
Diff to previous 91213
Renamed depends and dependents into subjects and observers.

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: 4655 byte(s)
Diff to previous 91205
AutoProof: Continued ownership translation.


Revision 91205 - (view) (annotate) - [select for diffs]
Modified Fri Feb 8 16:12:11 2013 UTC (6 years, 8 months ago) by julian
File length: 4586 byte(s)
Diff to previous 90127
AutoProof:
- Continued ownership translation.
- Added boxing/unboxing of integers and booleans.
- Added conversions between integer types.


Revision 90127 - (view) (annotate) - [select for diffs]
Modified Fri Dec 7 14:51:15 2012 UTC (6 years, 10 months ago) by julian
File length: 1318 byte(s)
Diff to previous 90118
Updated Boogie theory.

Revision 90118 - (view) (annotate) - [select for diffs]
Added Thu Dec 6 16:31:22 2012 UTC (6 years, 10 months ago) by julian
File length: 1113 byte(s)
Updated Boogie theory.

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