checker improvements

src/frama_c.py

@@ -300,8 +300,8 @@ def houdini(
                     code_queue.append("\n".join(code_lines))
 
             if "Annotation error " in checker_message:
-                # TODO: Why not remove all annotation errors?
-                # A: Frama-C panics and skips the entire annotation block
+                # Why not remove all annotation errors?
+                # Frama-C panics and skips the entire annotation block
                 # as soon as it sees an annotation error.
                 # So we get only one annotation error at a time.
                 annotation_error_line_no = self.get_line_no_from_error_msg(
@@ -310,12 +310,23 @@ def houdini(
 
                 if ": unexpected token ''" in checker_message:
                     # Some annotation has been emptied out
-                    # Remove the annotation
+                    # Remove the annotation and push the code to the queue
+                    # only if the code has changed
                     new_input_code = self.remove_empty_annotations(deepcopy(input_code))
+                    if new_input_code == input_code:
+                        Logger.log_error(
+                            "Stopping Houdini. Error message points to an empty line. Is the annotation malformed?"
+                        )
+                        break
                     code_queue.append(new_input_code)
                     continue
 
                 code_lines[annotation_error_line_no] = ""
+                if "\n".join(code_lines) == input_code:
+                    Logger.log_error(
+                        "Stopping Houdini. Error message points to an empty line. Is the annotation malformed?"
+                    )
+                    break
                 input_code = "\n".join(code_lines)
                 code_queue.append(input_code)
 
@@ -746,7 +757,7 @@ def combine_llm_outputs(self, checker_input, llm_outputs, features):
 
         invariants = {}
         variant = None
-        
+
         if "multiple_loops_one_method" == features:
             print("Combining invariants from {} outputs".format(len(llm_outputs)))