Relax requirement for naming functions in harnesses

rse-verification · May 29, 2024 · 8685fef · 8685fef
1 parent 3290165
commit 8685fef
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/src/saida_vis.ml b/src/saida_vis.ml
@@ -1015,7 +1015,11 @@ class acsl2tricera out = object (self)
             | TVoid _ -> ""
             | _ -> (get_type_decl_string hf.return_type) ^ " " ^ self#result_string ^ " = "
           in
-          self#print_line (s ^ "main2("^ params ^");\n");
+          let fname = curr_func.svar.vname in
+          if fname = "main" then
+            self#print_line (s ^ "main2("^ params ^");\n")
+          else
+            self#print_line (s ^ fname ^ "("^ params ^");\n");
         | None -> ();
     in
     (*Print the asserts, from the post-cond*)