/[eiffelstudio]
ViewVC logotype

Revision 95604


Jump to revision: Previous Next
Author: polikarn
Date: Tue Aug 12 17:08:39 2014 UTC (5 years, 1 month ago)
Changed paths: 49
Log Message:
Multiple changes to make AutoProof more predictable on big examples (simplified/optimized base theory, simplified type properties, inlined some checks, no generation of triggers by default, removed unused locals, strengthened inheritance axioms, new mechanism for type properties in logic classes, adjustible default update guards). Allow lemmas in logic classes. Bugfixes (including an unsound axiom for partial invariants).

Changed paths

Path Details
Directorybranches/eth/eve/Src/Delivery/studio/tools/autoproof/base_theory.bpl modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/e2b_messages.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/exec/e2b_result_generator.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_types.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/advanced/bags/a_bags.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/advanced/bags/output.txt modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/advanced/inheritance/output.txt modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/advanced/sequences/a_sequences.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/basic/references/b_references.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/comcom/array_sum/array_sum.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/comcom/sum_and_max/sum_and_max.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/composite/f_com_composite.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/composite/f_com_composite_d.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/observer_inheritance/f_oi_subject.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/observer_one_to_many/f_oom_subject.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/observer_one_to_many/f_oom_subject_d.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/pip/f_pip_client.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/pip/f_pip_node.e
(Copied from branches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/pip/f_pip_node2.e, r95603)
replaced , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/pip/f_pip_node2.e deleted
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/pip/f_pip_node2_d.e deleted
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/pip/f_pip_node_d.e
(Copied from branches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/pip/f_pip_node2_d.e, r95572)
replaced , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/pip/output.txt modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/custom/e2b_custom_logical_handler.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/custom/e2b_custom_ownership_handler.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_attribute_translator.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_body_expression_translator.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_entity_mapping.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_expression_translator.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_helper.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_instruction_translator.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_options.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_routine_translator.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_translator.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_type_translator.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/pool/e2b_translation_pool.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/pool/e2b_translation_unit.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/pool/e2b_tu_contract_check.e modified , text changed
Directorybranches/eth/eve/Src/library/base/base2/cell/v_linkable.e modified , text changed
Directorybranches/eth/eve/Src/library/base/eve/v_array.e modified , text changed
Directorybranches/eth/eve/Src/library/base/mml/bag.bpl modified , text changed
Directorybranches/eth/eve/Src/library/base/mml/map.bpl modified , text changed
Directorybranches/eth/eve/Src/library/base/mml/mml_bag.e modified , text changed
Directorybranches/eth/eve/Src/library/base/mml/mml_map.e modified , text changed
Directorybranches/eth/eve/Src/library/base/mml/mml_relation.e modified , text changed
Directorybranches/eth/eve/Src/library/base/mml/mml_sequence.e modified , text changed
Directorybranches/eth/eve/Src/library/base/mml/mml_set.e modified , text changed
Directorybranches/eth/eve/Src/library/base/mml/relation.bpl modified , text changed
Directorybranches/eth/eve/Src/library/base/mml/sequence.bpl modified , text changed
Directorybranches/eth/eve/Src/library/base/mml/set.bpl modified , text changed

  ViewVC Help
Powered by ViewVC 1.1.23