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

Diff of /branches/eth/eve/Src/framework/eiffel2boogie/translation/custom/e2b_custom_ownership_handler.e

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 93404 by julian, Thu Nov 14 15:57:08 2013 UTC revision 93405 by julian, Fri Nov 15 21:07:40 2013 UTC
# Line 93  feature -- Basic operations Line 93  feature -- Basic operations
93                                          a_translator.set_last_expression (                                          a_translator.set_last_expression (
94                                                  factory.function_call (                                                  factory.function_call (
95                                                          name_translator.boogie_name_for_filtered_invariant_function (a_translator.current_target_type, Void, l_tag_filters),                                                          name_translator.boogie_name_for_filtered_invariant_function (a_translator.current_target_type, Void, l_tag_filters),
96                                                          << a_translator.entity_mapping.heap, a_translator.entity_mapping.current_expression >>, types.bool))                                                          << a_translator.entity_mapping.heap, a_translator.current_target >>, types.bool))
97                                  elseif l_name ~ "inv_only" then                                  elseif l_name ~ "inv_only" then
98                                          l_tag_filters := extract_tags (a_parameters)                                          l_tag_filters := extract_tags (a_parameters)
99                                          translation_pool.add_filtered_invariant_function (a_translator.current_target_type, l_tag_filters, Void)                                          translation_pool.add_filtered_invariant_function (a_translator.current_target_type, l_tag_filters, Void)
100                                          a_translator.set_last_expression (                                          a_translator.set_last_expression (
101                                                  factory.function_call (                                                  factory.function_call (
102                                                          name_translator.boogie_name_for_filtered_invariant_function (a_translator.current_target_type, l_tag_filters, Void),                                                          name_translator.boogie_name_for_filtered_invariant_function (a_translator.current_target_type, l_tag_filters, Void),
103                                                          << a_translator.entity_mapping.heap, a_translator.entity_mapping.current_expression >>, types.bool))                                                          << a_translator.entity_mapping.heap, a_translator.current_target >>, types.bool))
104                                  else                                  else
105                                          a_translator.process_builtin_routine_call (a_feature, a_parameters, l_name)                                          a_translator.process_builtin_routine_call (a_feature, a_parameters, l_name)
106                                  end                                  end

Legend:
Removed from v.93404  
changed lines
  Added in v.93405

  ViewVC Help
Powered by ViewVC 1.1.23