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

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

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 93733 - (view) (annotate) - [select for diffs]
Modified Mon Dec 16 12:32:04 2013 UTC (5 years, 9 months ago) by polikarn
File length: 41550 byte(s)
Diff to previous 93731
Changed handling of default initialization in creators: free preconditions instead of assignment; precondition is_open now cannot be disabled since there is no choice.

Revision 93731 - (view) (annotate) - [select for diffs]
Modified Mon Dec 16 09:25:16 2013 UTC (5 years, 9 months ago) by polikarn
File length: 41063 byte(s)
Diff to previous 93728
Bugfix in precondition predicate generation. Fixed tests.

Revision 93728 - (view) (annotate) - [select for diffs]
Modified Sun Dec 15 15:00:11 2013 UTC (5 years, 10 months ago) by polikarn
File length: 41297 byte(s)
Diff to previous 93726
Arguments as default variants.

Revision 93726 - (view) (annotate) - [select for diffs]
Modified Sun Dec 15 12:57:21 2013 UTC (5 years, 10 months ago) by polikarn
File length: 40941 byte(s)
Diff to previous 93715
Checking preconditions of functionals.

Revision 93715 - (view) (annotate) - [select for diffs]
Modified Fri Dec 13 16:48:35 2013 UTC (5 years, 10 months ago) by polikarn
File length: 39474 byte(s)
Diff to previous 93713
Allowing checks in functionals.

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: 38980 byte(s)
Diff to previous 93706
Removed some unnecessary checks, added semantic warnings.

Revision 93706 - (view) (annotate) - [select for diffs]
Modified Thu Dec 12 22:19:59 2013 UTC (5 years, 10 months ago) by polikarn
File length: 38930 byte(s)
Diff to previous 93704
Refactoring of the feature translation process; functional features now have boogie procedures to perform checks (e.g. termination).

Revision 93704 - (view) (annotate) - [select for diffs]
Modified Thu Dec 12 15:02:44 2013 UTC (5 years, 10 months ago) by polikarn
File length: 40150 byte(s)
Diff to previous 93665
Decreases checks (except functional features).

Revision 93665 - (view) (annotate) - [select for diffs]
Modified Mon Dec 9 16:43:50 2013 UTC (5 years, 10 months ago) by polikarn
File length: 40350 byte(s)
Diff to previous 93640
Added old function for old expressions in the body. Made the trigger of global more restrictive for performance purposes.

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: 40074 byte(s)
Diff to previous 93637
AutoProof: finished refactoring of error display.

Revision 93637 - (view) (annotate) - [select for diffs]
Modified Fri Dec 6 11:50:07 2013 UTC (5 years, 10 months ago) by julian
File length: 39937 byte(s)
Diff to previous 93633
AutoProof: added stop button.
AutoProof: improved error messages.

Revision 93633 - (view) (annotate) - [select for diffs]
Modified Fri Dec 6 01:24:52 2013 UTC (5 years, 10 months ago) by julian
File length: 38523 byte(s)
Diff to previous 93627
AutoProof: refactoring of error message display.

Revision 93627 - (view) (annotate) - [select for diffs]
Modified Thu Dec 5 16:42:21 2013 UTC (5 years, 10 months ago) by julian
File length: 38531 byte(s)
Diff to previous 93605
AutoProof: continued refactoring of output parser.

Revision 93605 - (view) (annotate) - [select for diffs]
Modified Tue Dec 3 10:10:31 2013 UTC (5 years, 10 months ago) by polikarn
File length: 38569 byte(s)
Diff to previous 93597
Adding global heap property as a precondition for lemmas + refactoring.

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

Revision 93583 - (view) (annotate) - [select for diffs]
Modified Fri Nov 29 18:50:14 2013 UTC (5 years, 10 months ago) by polikarn
File length: 35212 byte(s)
Diff to previous 93574
Sequence theory is now 1-based. Fixed unsoundness in loop writes. Optimized global invariant in the bg theory. OOM verifies.

Revision 93574 - (view) (annotate) - [select for diffs]
Modified Thu Nov 28 18:19:34 2013 UTC (5 years, 10 months ago) by polikarn
File length: 35216 byte(s)
Diff to previous 93571
Changed semantics of modify_field from nett effect to local.

Revision 93571 - (view) (annotate) - [select for diffs]
Modified Thu Nov 28 12:53:21 2013 UTC (5 years, 10 months ago) by polikarn
File length: 35713 byte(s)
Diff to previous 93569
Added routine frames on loops.

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: 36093 byte(s)
Diff to previous 93568
AutoProof: added support for comparing sets and sequences

Revision 93568 - (view) (annotate) - [select for diffs]
Modified Thu Nov 28 08:51:15 2013 UTC (5 years, 10 months ago) by julian
File length: 35978 byte(s)
Diff to previous 93557
AutoProof: better error handling for modifies clauses.

Revision 93557 - (view) (annotate) - [select for diffs]
Modified Wed Nov 27 17:46:18 2013 UTC (5 years, 10 months ago) by polikarn
File length: 35853 byte(s)
Diff to previous 93532
Added HeapSucc. Changed translation of object test.

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

Revision 93528 - (view) (annotate) - [select for diffs]
Modified Mon Nov 25 20:45:28 2013 UTC (5 years, 10 months ago) by polikarn
File length: 36504 byte(s)
Diff to previous 93523
Replaced the Writes variable by a constant with a free precondition.

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: 36870 byte(s)
Diff to previous 93482
AutoProof: added better feedback for unsupported code.

Revision 93482 - (view) (annotate) - [select for diffs]
Modified Wed Nov 20 19:31:39 2013 UTC (5 years, 10 months ago) by julian
File length: 36817 byte(s)
Diff to previous 93479
AutoProof: Added FM2012 examples

Revision 93479 - (view) (annotate) - [select for diffs]
Modified Wed Nov 20 17:48:43 2013 UTC (5 years, 10 months ago) by polikarn
File length: 37606 byte(s)
Diff to previous 93417
Added types and tags to default pre- and postconditions.

Revision 93417 - (view) (annotate) - [select for diffs]
Modified Mon Nov 18 17:29:07 2013 UTC (5 years, 10 months ago) by julian
File length: 35987 byte(s)
Diff to previous 93378
AutoProof: verified composite example.

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


Revision 93364 - (view) (annotate) - [select for diffs]
Modified Thu Nov 14 08:30:25 2013 UTC (5 years, 11 months ago) by julian
File length: 35276 byte(s)
Diff to previous 93319
AutoProof: added defaults for modifies clauses.

Revision 93319 - (view) (annotate) - [select for diffs]
Modified Tue Nov 12 17:05:13 2013 UTC (5 years, 11 months ago) by julian
File length: 34866 byte(s)
Diff to previous 93306
AutoProof: improved some ownership examples.

Revision 93306 - (view) (annotate) - [select for diffs]
Modified Mon Nov 11 16:45:33 2013 UTC (5 years, 11 months ago) by julian
File length: 34755 byte(s)
Diff to previous 93272
AutoProof: Continued with ownership implementation.
AutoProof: Added PIP example and fixed OOM example.

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

Revision 93242 - (view) (annotate) - [select for diffs]
Modified Thu Nov 7 09:57:40 2013 UTC (5 years, 11 months ago) by julian
File length: 30939 byte(s)
Diff to previous 93215
AutoProof: continued ownership implementation.

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

Revision 93206 - (view) (annotate) - [select for diffs]
Modified Tue Nov 5 16:52:31 2013 UTC (5 years, 11 months ago) by julian
File length: 30225 byte(s)
Diff to previous 93203
AutoProof: continued ownership implementation.

Revision 93203 - (view) (annotate) - [select for diffs]
Modified Tue Nov 5 08:18:31 2013 UTC (5 years, 11 months ago) by julian
File length: 30221 byte(s)
Diff to previous 93193
AutoProof: continue on ownership implementation.

Revision 93193 - (view) (annotate) - [select for diffs]
Modified Mon Nov 4 16:38:13 2013 UTC (5 years, 11 months ago) by julian
File length: 34752 byte(s)
Diff to previous 93175
AutoProof: continue on 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: 34735 byte(s)
Diff to previous 92868
AutoProof: initial refactoring for routine translators.
AutoProof: added two examples.

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: 34754 byte(s)
Diff to previous 92762
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 92762 - (view) (annotate) - [select for diffs]
Modified Mon Jul 1 16:00:14 2013 UTC (6 years, 3 months ago) by polikarn
File length: 34508 byte(s)
Diff to previous 92724
Added some tests for MML_SET features

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: 34440 byte(s)
Diff to previous 91348
Renamed depends and dependents into subjects and observers.

Revision 91348 - (view) (annotate) - [select for diffs]
Modified Fri Mar 8 15:59:40 2013 UTC (6 years, 7 months ago) by julian
File length: 34440 byte(s)
Diff to previous 91302
AutoProof: added predicates for arithmetic operations. added suggestion display for two-step verification.



Revision 91302 - (view) (annotate) - [select for diffs]
Modified Wed Feb 27 17:09:56 2013 UTC (6 years, 7 months ago) by julian
File length: 34417 byte(s)
Diff to previous 91221
AutoProof: enabled invariant generation. updated array translation.

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: 32494 byte(s)
Diff to previous 91213
AutoProof: update to Array translation.

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: 32527 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: 32438 byte(s)
Diff to previous 91096
AutoProof:
- Continued ownership translation.
- Added boxing/unboxing of integers and booleans.
- Added conversions between integer types.


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: 31770 byte(s)
Diff to previous 90229
Separate Boogie translation for creation routines.
Added incomplete ownership translation.

Revision 90229 - (view) (annotate) - [select for diffs]
Modified Mon Dec 17 08:51:21 2012 UTC (6 years, 9 months ago) by julian
File length: 26776 byte(s)
Diff to previous 90191
Improved error reporting for AutoProof.

Revision 90191 - (view) (annotate) - [select for diffs]
Modified Fri Dec 14 15:38:20 2012 UTC (6 years, 10 months ago) by julian
File length: 26731 byte(s)
Diff to previous 90072
Updated Boogie theory.

Revision 90072 - (view) (annotate) - [select for diffs]
Modified Sat Dec 1 15:51:18 2012 UTC (6 years, 10 months ago) by julian
File length: 26413 byte(s)
Diff to previous 89959
Updated Boogie theory.

Revision 89959 - (view) (annotate) - [select for diffs]
Modified Wed Nov 21 15:11:49 2012 UTC (6 years, 10 months ago) by julian
File length: 26409 byte(s)
Diff to previous 89947
Fixed issues with Boogie translation.

Revision 89947 - (view) (annotate) - [select for diffs]
Modified Mon Nov 19 09:17:10 2012 UTC (6 years, 10 months ago) by julian
File length: 26135 byte(s)
Diff to previous 89744
Refactoring of AutoProof result display.

Revision 89744 - (view) (annotate) - [select for diffs]
Modified Tue Oct 30 08:46:37 2012 UTC (6 years, 11 months ago) by julian
File length: 26029 byte(s)
Diff to previous 88727
Added AutoProof command to context menu.
Added simple tool for AutoProof to select options.
Updated Boogie output parser to new Boogie version.

Revision 88727 - (view) (annotate) - [select for diffs]
Modified Tue May 15 08:10:56 2012 UTC (7 years, 5 months ago) by julian
File length: 25662 byte(s)
Diff to previous 88710
Added tracing information for generating error model.

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: 25769 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