def line_as_comment(line):
    """Change a C code line to a comment by adding the prefix "// "

    If the last character of the line is a backslash, certain
    characters are appended. This silences some compiler warnings.
    """
    line = "// " + line
    if line[-2:] == "\\\n": 
        line = line[:-2] +  "\\ //\n"
    return line