代写C++编程、代做program程序设计

日期：2024-01-12 08:59

Problem 1

This 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++

Automated Software Verification 2023/2024

Coursework 2

programs:

https://www.cprover.org/cbmc/

Question 1 [25 marks] The following C code for computing the greatest common divisor of

two positive integer numbers contains a fault:

#include <stdio.h>

//Euclidean algorithm

int 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 2

Because Frama-C is only available on MacOS and Linux, the students who only have access

to a Windows computer should team up with a single other student. Although you can work

as a team on the assignment, both members of the team still should submit the solutions to

all problems individually.

Download and install Frama-C:

http://frama-c.com/

Question 1 [25 marks] Annotate the given code by specifying appropriate loop invariants

and verify the assert statement using Frama-C. The assert statement is already given in the

code.

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 is

checkable by Frama-C. [5 marks]

3. Briefly describe the reasoning process you have gone through in order to arrive at the

solution. [10 marks]

Question 2 [25 marks] Annotate the given code by specifying appropriate loop invariants

and verify the assert statement using Frama-C. The assert statement is already given in the

code.

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 is

checkable by Frama-C. [5 marks]

3. Briefly describe the reasoning process you have gone through in order to arrive at the

solution. [10 marks]

Submit a single PDF file not exceeding 2MB in size. Change your screenshots to a lower

resolution, if needed.