Automated Software Verification 2023/2024Coursework 2Problem 1This is an individual problem. Each student must work on it alone and submit her/his solution individually. Download and install CBMC is a Bounded Model Checker for C and C++programs:https://www.cprover.org/cbmc/Question 1 [25 marks] The following C code for computing the greatest common divisor oftwo positive integer numbers contains a fault:#include <stdio.h>//Euclidean algorithmint gcd(int a, int b) {return gcd(b % a, a);}int main() {int a = 5, b = 2;printf("gcd(%d, %d) = %d\n.", a, b, gcd(a, b));a = 50, b = 6;printf("gcd(%d, %d) = %d\n.", a, b, gcd(a, b));return 0;}1. Provide the CBMC command line input/output which exposes the fault. [5 marks]2. Explain the problem with the code. [10 marks]3. Fix the problem, include the new version of the code into your submission. [10 marks]Question 2 [25 marks] The following C code also contains a fault:#include<stdio.h>int main() {char c;char message[64];int i = 0;while( ((c = getchar()) != '.')) {message[i] = c;i++;}printf("Thank you for your feedback!");return 0;}1. Provide the CBMC command line input/output which exposes the fault. [5 marks]2. Explain the problem with the code. [10 marks]3. Fix the problem, include the new version of the code into your submission. [10 marks]Problem 2Because Frama-C is only available on MacOS and Linux, the students who only have accessto a Windows computer should team up with a single other student. Although you can workas a team on the assignment, both members of the team still should submit the solutions toall problems individually.Download and install Frama-C:http://frama-c.com/Question 1 [25 marks] Annotate the given code by specifying appropriate loop invariantsand verify the assert statement using Frama-C. The assert statement is already given in thecode.int main(){int a = 0;int s = 0;while(a != 10){a++;int b = 0;while(b != 10){b++;s++;}}//@assert s == 100;}1. Submit a printout of the annotated version of the code. [10 marks]2. Submit a screenshot (with green marks) of Frama-C window showing that your code ischeckable by Frama-C. [5 marks]3. Briefly describe the reasoning process you have gone through in order to arrive at thesolution. [10 marks]Question 2 [25 marks] Annotate the given code by specifying appropriate loop invariantsand verify the assert statement using Frama-C. The assert statement is already given in thecode.int f(int x){return x+1;}void test(){int s = 20;int i = 0;while (i<10){s=f(s);i++;}//@assert s==30;}1. Submit a printout of the annotated version of the code. [10 marks]2. Submit a screenshot (with green marks) of Frama-C window showing that your code ischeckable by Frama-C. [5 marks]3. Briefly describe the reasoning process you have gone through in order to arrive at thesolution. [10 marks]Submit a single PDF file not exceeding 2MB in size. Change your screenshots to a lowerresolution, if needed.