Homework 1

Write a C-program that implements a queue of an answering machine with space for 100 messages. The queue should be able to store messages consisting of:

-a first name, of at most 15 characters,
-a last name, of at most 25 characters,
-a social security number of length 10.

The C program shall have the following two functions:

-void copy(char s1[], int n1, char s2[], int n2), which copies as many characters as possible in the array s2 to the array s1, where n1 is the length of s1 and n2 is the length of s2.
-void leave_message(char first_name[], int n1, char last_name[], int n2, char social_security_number[], int n3). Leave message should work as follows. If there is free space in the queue, then first_name, of length n1 => 0, last_name, of length n2 => 0, and social_security_number, of length n3 => 0, are copied into the queue, by means of the copy function, where the previous entries in the queue are unchanged. The return value is 0 to denote success. If there is no free space in the queue, then the queue is unchanged and -1 is returned to denote failure.

It is assumed that all arrays are non-overlapping.

Annotate your functions and verify it by means of the WP plugin of Frama-C.

To get a bonus point, it is sufficient to write the C program and make a serious attempt to annotate it such that WP accepts the annotations. It is not required that Frama-C accepts all annotations.

It might be useful to read up on the following builtin constructs of ACSL (see the specification at https://frama-c.com/download/acsl_1.13.pdf): \separated, \forall, \at, assigns, loop invariant, loop assigns, and \result. Also the behavior construct might be useful.