io_frontend header with new functions

include/io_frontend.h

@@ -23,6 +23,9 @@ extern void _put_bool(FILE* file, char* n, _Bool _V);
 extern void _put_int(FILE* file, char* n, int _V);
 
 /*@ assigns \nothing; */
-extern void _put_double(FILE* file, char* n, double _V);
+extern void _put_float(FILE* file, char* n, float _V, int PREC);
+
+/*@ assigns \nothing; */
+extern void _put_double(FILE* file, char* n, double _V, int PREC);
 
 #endif

include/io_frontend.hpp

@@ -80,15 +80,30 @@ void _put_int(FILE* file, char* n, int _V){
   printf("\n");
   fprintf(file, "%d\n", _V);
 }
-void _put_double(FILE* file, char* n, double _V){
+
+void _put_float(FILE* file, char* n, float _V, int PREC){
+  if(ISATTY) {
+    printf("%s = ", n);
+  } else {
+    printf("'%s': ", n);
+  };
+  printf("'%.*f' ", PREC, _V);
+  printf("\n");
+  fprintf(file, "%.*f\n", PREC, _V);
+  fflush(file);
+}
+
+void _put_double(FILE* file, char* n, double _V, int PREC){
   if(ISATTY) {
     printf("%s = ", n);
   } else {
     printf("'%s': ", n);
   };
-  printf("'%f' ", _V);
+  printf("'%.*f' ", PREC, _V);
   printf("\n");
-  fprintf(file, "%f\n", _V);
+  fprintf(file, "%.*f\n", PREC, _V);
+  fflush(file);
 }
 
+
 #endif