/[eiffelstudio]
ViewVC logotype

Revision 85735


Jump to revision: Previous Next
Author: jasonw
Date: Sun Feb 27 15:15:17 2011 UTC (8 years, 6 months ago)
Changed paths: 11
Log Message:
Used Boogie to verify that certain expressions are valid with respect to class invariants. Those valid expressions won't be considered as targets of the AutoTest precondition reduction strategy.

Changed paths

Path Details
Directorybranches/eth/eve/Src/framework/auto_fix/utility/afx_utility.e modified , text changed
Directorybranches/eth/eve/Src/framework/auto_test/strategy/precondition_reduction/aut_precondition_reduction_strategy.e modified , text changed
Directorybranches/eth/eve/Src/framework/auto_test/strategy/precondition_reduction/aut_prestate_invariant_loader.e modified , text changed
Directorybranches/eth/eve/Src/framework/auto_test/strategy/precondition_reduction/expressions/aut_state_invariant.e modified , text changed
Directorybranches/eth/eve/Src/framework/program_analysis/contract/epa_postcondition_as_invariant_generator.e modified , text changed
Directorybranches/eth/eve/Src/framework/program_analysis/solver_utility/epa_shared_class_theory.e modified , text changed
Directorybranches/eth/eve/Src/framework/program_analysis/solver_utility/epa_solver_expression_generator.e modified , text changed
Directorybranches/eth/eve/Src/framework/program_analysis/solver_utility/epa_solver_factory.e modified , text changed
Directorybranches/eth/eve/Src/framework/semantic_search/kernel/sem_constants.e modified , text changed
Directorybranches/eth/eve/Src/framework/semantic_search/query/sem_property_printer.e modified , text changed
Directorybranches/eth/eve/Src/framework/semantic_search/query/sem_simple_query_generator.e modified , text changed

  ViewVC Help
Powered by ViewVC 1.1.23