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(OutStream & 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 !