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
//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
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.