pdg and PostDomination in C Programs

برای نصب frama-c بر روی ubuntu ابتدا در ترمینال دستور زیر را وارد مینماییم

sudo apt-get install frama-c

در اینجا باید منتظر بمانیم تا پکیج های وابسته به اضافه ی خود frama-c دانلود گردد و نصب شود.

پکیج های زیر را نیز باید نصب نماییم و دستور زیر را در تریمینال اجرا میکنیم.

sudo apt-get install ocaml ocaml-native-compilers graphviz libzarith-ocaml-dev libfindlib-ocaml-dev  liblablgtksourceview2-ocaml-dev liblablgtk2-gnome-ocaml-dev

سپس در تریمنال y را مینویسیم و منتظر میمانیم تا دانلود و نصب گردند.

#include <stdio.h>
void hello() {
printf("\n#################################\n   National Code Validator By\n        Shadi Bagheri \n#################################\n\n\n");
}
int main() {
    hello();
    long nationalCode;
    int count = 0;
    long invalidCodes[] = {
        1111111111,
        2222222222,
        3333333333,
        4444444444,
        5555555555,
        6666666666,
        7777777777,
        8888888888,
        9999999999,
        0000000000
    };
    int array[9];
    int sum = 0;
    int controlNum;
   int recurrent; 
   printf("Enter a National Code: ");
    scanf("%ld", &nationalCode);
    for(int i = 0; i <= 9; i++) {
 if(invalidCodes[i] == nationalCode) {
  printf("Invalid \n");
   return 0;
   }
    }
    for(int i = 0; i <= 9; i++) {
        array[i] = nationalCode % 10;
        nationalCode /= 10;
    }
    int j = 1;
    for(int i = 1; i <= 9; i++) {
        sum += ++j * array[i];
    }
controlNum = array[0];
    recurrent = sum % 11;
    if( (recurrent > 1) && (controlNum == (11 - recurrent)) ) {
    printf("Valid \n");
        return 1;
    } else if(recurrent == 0 && controlNum == 0) {
        printf("Valid \n");
        return 1;
    } else if(recurrent == 1 && controlNum == 1) {
        printf("Valid \n");
        return 1;
    } else {\
        printf("Invalid \n");
        return 0;
    }
    printf("Invalid \n");
    return 0;
}

توضیحاتی درباره عملکرد برنامه:
تایید شماره ملی:
هر شماره ملی دارای 10رقم میباشد و رقم آخر (چپ ترین) رقم کنترلی می باشد.
برای صحت کد ملی باید 9رقم اول را برعکس نوشت و در جایگاه هایشان ضرب کرد.
سپس عدد بدست آمده را در 11تقسیم کرد.
در صورتی که باقی مانده با رقم کنترل برابر باشد، شماره ملی وارد شده، صحیح است.
این برنامه، نیز شماره ملی های وارد شده را بررسی میکند.

کد بالا را در یک فایل با نام main.c ذخیره میکنیم.

اکنون با دستور زیر فایل main.c را در frama-c اجرا میکنیم

frama-c-gui main.c

محیط برنامه به شکل زیر باز میگردد:

callgraph:

از تب analyses به منوی analyses میرویم پنجره ی زیر باز میگردد:

روی execute کیلک میکنیم سپس برای مشاهده ی گراف ، بر روی analyses و بعد show callgraph کلیک می کنیم.

Post domination:

برای به دست آوردن post domination کد در ترمینال کد زیر را اجرا می کنیم

frama-c main.c -dot-postdom main

دستور زیر pdf گراف post domination را به ما می دهد

dot  -Tpdf main.main.dot > postdom.pdf

PDG:

برای به دست آوردن گراف pdg کد مربوطه دستور زیر را اجرا مینماییم:

frama-c -pdg -pdg-dot graph -pdg-print main.c > pdg.dot

برای دیدن گراف به صورت pdf دستور زیر را در ترمینال اجرا می کنیم:

dot -Tpdf graph.main.dot > pdg.pdf

به دلیل پیچیده بودن گراف pdg در سه مرحله از گراف screenshot تهیه نمودیم.