CIS-5130 Homework #3 (Frama-C and EVA)

Consider the program converter.c that converts an input file from UTF-8 encoded Unicode characters to UTF-16 encoded Unicode characters. This program contains the function decode_UTF8 that takes an 8 bit value (from the input file) and assumes it is the lead byte of a UTF-8 encoded character. It returns the 32 bit Unicode "code point" corresponding to that character. To do this it might need to read the input file several more times. See Wikipedia's page on UTF-8 for more information about the encoding.

Using Frama-C's EVA plug-in, analyze this function to ensure that the value assigned to code_point in each branch of the if... else... is in a sensible range.

You will have to think about several things, and you may need to look up how to best solve these issues.

Write a document that describes what you did, maybe including any driver program or stub functions, if appropriate, and that summarizes the results of your analysis. Submit your document to Moodle.