La palteforme est constituée des projets suivants:
Projet | Descritption |
---|---|
org.eclipse.efm.sep.doc | Documentation, architecture générale |
org.eclipse.efm.sep.common | Eléments communs |
org.eclipse.efm.sep.core | Eléments de base |
org.eclipse.efm.sep.infra | Infrastructure de données |
org.eclipse.efm.sep.fam | Modules d'analyse formalle |
org.eclipse.efm.sep.solver | Services de solver |
org.eclipse.efm.sep.engine | Le moteur |
org.eclipse.efm.sep.workflow | Le workflow |
Chaque projet est constitué des sections suivante:
Utilitaires communs à tous les autres composants
services de sérialisation services de gestion de trace de mise au point
Les détails d'implémentation interne !
Les détails d'implémentation interne !
Infrastructure pour l'exécution symbolique
Les détails d'implémentation interne !
Module d'Analyse Formelle
C‘est l’interface que doit implémenter tout Module d'Analyse Formelle. Il fournit des services pour intervenir dans les différentes phases du SEW, Symbolic Execution Workflow, à savoir:
configure, MANDATORY
preprocess, OPTIONAL, s'il a un traitement à effectuer, en preprocessing, i.e. avant la phase dynamique du processus Diversity
postprocess, OPTIONAL, s'il a un traitement à effectuer, en postprocessing, i.e. après la phase dynamique du processus Diversity
prefilter, OPTIONAL, s‘il a un traitement à effectuer, en prefiltering, i.e. pendant la phase dynamique du processus Diversity , mais avant l’exécution symbolique proprement dite
postfilter, OPTIONAL, s‘il a un traitement à effectuer, en postfiltering, i.e. pendant la phase dynamique du processus Diversity , mais après l’exécution symbolique proprement dite
report, OPTIONAL, pour proposer un bilan de l'analyse formelle effectuée
Soit par exemple:
class MyFAM : public AutoRegisteredFAM< MyFAM >, { // MANDATORY for Smart Pointer services AVM_DECLARE_CLONABLE_CLASS( MyFAM ) /** * MyFAM * for automatic registration in the FAM repository * the UFID key * need for instanciation from the SEW specification file */ AVM_INJECT_AUTO_REGISTER_UFID_KEY( "MyFAM" ) // end registration protected: /** * ATTRIBUTE */ public: /** * CONSTRUCTOR */ MyFAM(CentralProcessorUnit & aManager, Form * aParameterForm) : AutoRegisteredFAM(aManager, aParameterForm, AVM_PRE_FILTERING_STAGE | AVM_POST_FILTERING_STAGE, ...), /** * CONFIGURE */ bool configureImpl(); /** * REPORT TRACE */ virtual void reportDefault(AvmOstream & os) const; //////////////////////////////////////////////////////////////////////////// // PROCESSING API //////////////////////////////////////////////////////////////////////////// /** * preProcessing */ virtual bool preprocess(); /** * postprocessing */ virtual bool postprocess(); //////////////////////////////////////////////////////////////////////////// // FILTERING API //////////////////////////////////////////////////////////////////////////// /** * preFiltering */ virtual bool prefilter(ExecutionContext * anEC); /** * postFiltering * Every post filter has to implement this method */ virtual bool postfilter(ExecutionContext * anEC); };
C‘est le scheduler qui gère l’activation les FAMs dans les différentes phases de l'exécution (voir section MOE dans le fichier SEW/FAVM de spécification du workflow)
C'est le FAM principal, toujours actif, ayant la charge de
Les détails d'implémentation interne !
org.eclipse.efm.sep.common
org.eclipse.efm.sep.core
org.eclipse.efm.sep.infra
org.eclipse.efm.sep.solver.ISolver défini l‘interface des services attendus d’un solver, pour un prédicat booléen donné, tel:
org.eclipse.efm.sep.solver.SolverFactory est une factory permettant:
Les détails d'implémentation interne !
Instancie et exécute la plateforme d'analyse symbolique définie dans le workflow
org.eclipse.efm.sep.
L'exécutable résultant
Les détails d'implémentation interne !
Les détails d'implémentation interne !