/[eiffelstudio]
ViewVC logotype

Revision 92856


Jump to revision: Previous Next
Author: julian
Date: Tue Aug 6 13:21:35 2013 UTC (6 years, 1 month ago)
Changed paths: 16
Log Message:
Integrated loop invariant inference code by Michael Ameri

Changed paths

Path Details
Directorybranches/eth/eve/Src/Eiffel/interface/graphical/tools/autoproof/es_autoproof_tool_panel.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/exec/e2b_output_parser.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/exec/result/e2b_successful_verification.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/inference/ added
Directorybranches/eth/eve/Src/framework/eiffel2boogie/inference/e2b_loop_inv_inference_by_mutation.e added
Directorybranches/eth/eve/Src/framework/eiffel2boogie/inference/e2b_postcondition_mutation_visitor.e added
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_attach_invariant.e added
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_block.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_comparer.e added
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_expression_2_eiffel_postcondition.e added
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_expression_replacer.e added
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_map_access.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tasks/e2b_postcondition_mutation_task.e added
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tasks/e2b_verify_task.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_name_translator.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_options.e modified , text changed

  ViewVC Help
Powered by ViewVC 1.1.23