remove mathematical_typet() constructor, which produces an incomplete object

kroening · kroening · commit 1fe7cd701905 · 2018-05-29T17:34:00.000+01:00
diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp
@@ -1028,26 +1028,27 @@ typet smt2_parsert::function_signature_definition()
     return sort();
   }
 
-  mathematical_function_typet result;
+  mathematical_function_typet::domaint domain;
 
   while(peek()!=CLOSE)
   {
     if(next_token()!=OPEN)
     {
       error() << "expected '(' at beginning of parameter" << eom;
-      return result;
+      return nil_typet();
     }
 
     if(next_token()!=SYMBOL)
     {
       error() << "expected symbol in parameter" << eom;
-      return result;
+      return nil_typet();
     }
 
-    auto &var=result.add_variable();
+    mathematical_function_typet::variablet var;
     std::string id=buffer;
     var.set_identifier(id);
     var.type()=sort();
+    domain.push_back(var);
 
     auto &entry=id_map[id];
     entry.type=var.type();
@@ -1056,15 +1057,15 @@ typet smt2_parsert::function_signature_definition()
     if(next_token()!=CLOSE)
     {
       error() << "expected ')' at end of parameter" << eom;
-      return result;
+      return nil_typet();
     }
   }
 
   next_token(); // eat the ')'
 
-  result.codomain()=sort();
+  typet codomain = sort();
 
-  return result;
+  return mathematical_function_typet(domain, codomain);
 }
 
 typet smt2_parsert::function_signature_declaration()
@@ -1081,37 +1082,38 @@ typet smt2_parsert::function_signature_declaration()
     return sort();
   }
 
-  mathematical_function_typet result;
+  mathematical_function_typet::domaint domain;
 
   while(peek()!=CLOSE)
   {
     if(next_token()!=OPEN)
     {
       error() << "expected '(' at beginning of parameter" << eom;
-      return result;
+      return nil_typet();
     }
 
     if(next_token()!=SYMBOL)
     {
       error() << "expected symbol in parameter" << eom;
-      return result;
+      return nil_typet();
     }
 
-    auto &var=result.add_variable();
+    mathematical_function_typet::variablet var;
     var.type()=sort();
+    domain.push_back(var);
 
     if(next_token()!=CLOSE)
     {
       error() << "expected ')' at end of parameter" << eom;
-      return result;
+      return nil_typet();
     }
   }
 
   next_token(); // eat the ')'
 
-  result.codomain()=sort();
+  typet codomain = sort();
 
-  return result;
+  return mathematical_function_typet(domain, codomain);
 }
 
 void smt2_parsert::command(const std::string &c)
diff --git a/src/util/std_types.h b/src/util/std_types.h
@@ -1686,11 +1686,6 @@ inline complex_typet &to_complex_type(typet &type)
 class mathematical_function_typet:public typet
 {
 public:
-  mathematical_function_typet():typet(ID_mathematical_function)
-  {
-    subtypes().resize(2);
-  }
-
   // the domain of the function is composed of zero, one, or
   // many variables
   class variablet:public irept
@@ -1720,6 +1715,14 @@ class mathematical_function_typet:public typet
 
   using domaint=std::vector<variablet>;
 
+  mathematical_function_typet(const domaint &_domain, const typet &_codomain)
+    : typet(ID_mathematical_function)
+  {
+    subtypes().resize(2);
+    domain() = _domain;
+    codomain() = _codomain;
+  }
+
   domaint &domain()
   {
     return (domaint &)subtypes()[0].subtypes();

Original file line number	Diff line number	Diff line change
`@@ -1028,26 +1028,27 @@ typet smt2_parsert::function_signature_definition()`
`1028`	`1028`	`return sort();`
`1029`	`1029`	`}`
`1030`	`1030`
`1031`		`- mathematical_function_typet result;`
	`1031`	`+ mathematical_function_typet::domaint domain;`
`1032`	`1032`
`1033`	`1033`	`while(peek()!=CLOSE)`
`1034`	`1034`	`{`
`1035`	`1035`	`if(next_token()!=OPEN)`
`1036`	`1036`	`{`
`1037`	`1037`	`error() << "expected '(' at beginning of parameter" << eom;`
`1038`		`- return result;`
	`1038`	`+ return nil_typet();`
`1039`	`1039`	`}`
`1040`	`1040`
`1041`	`1041`	`if(next_token()!=SYMBOL)`
`1042`	`1042`	`{`
`1043`	`1043`	`error() << "expected symbol in parameter" << eom;`
`1044`		`- return result;`
	`1044`	`+ return nil_typet();`
`1045`	`1045`	`}`
`1046`	`1046`
`1047`		`- auto &var=result.add_variable();`
	`1047`	`+ mathematical_function_typet::variablet var;`
`1048`	`1048`	`std::string id=buffer;`
`1049`	`1049`	`var.set_identifier(id);`
`1050`	`1050`	`var.type()=sort();`
	`1051`	`+ domain.push_back(var);`
`1051`	`1052`
`1052`	`1053`	`auto &entry=id_map[id];`
`1053`	`1054`	`entry.type=var.type();`
`@@ -1056,15 +1057,15 @@ typet smt2_parsert::function_signature_definition()`
`1056`	`1057`	`if(next_token()!=CLOSE)`
`1057`	`1058`	`{`
`1058`	`1059`	`error() << "expected ')' at end of parameter" << eom;`
`1059`		`- return result;`
	`1060`	`+ return nil_typet();`
`1060`	`1061`	`}`
`1061`	`1062`	`}`
`1062`	`1063`
`1063`	`1064`	`next_token(); // eat the ')'`
`1064`	`1065`
`1065`		`- result.codomain()=sort();`
	`1066`	`+ typet codomain = sort();`
`1066`	`1067`
`1067`		`- return result;`
	`1068`	`+ return mathematical_function_typet(domain, codomain);`
`1068`	`1069`	`}`
`1069`	`1070`
`1070`	`1071`	`typet smt2_parsert::function_signature_declaration()`
`@@ -1081,37 +1082,38 @@ typet smt2_parsert::function_signature_declaration()`
`1081`	`1082`	`return sort();`
`1082`	`1083`	`}`
`1083`	`1084`
`1084`		`- mathematical_function_typet result;`
	`1085`	`+ mathematical_function_typet::domaint domain;`
`1085`	`1086`
`1086`	`1087`	`while(peek()!=CLOSE)`
`1087`	`1088`	`{`
`1088`	`1089`	`if(next_token()!=OPEN)`
`1089`	`1090`	`{`
`1090`	`1091`	`error() << "expected '(' at beginning of parameter" << eom;`
`1091`		`- return result;`
	`1092`	`+ return nil_typet();`
`1092`	`1093`	`}`
`1093`	`1094`
`1094`	`1095`	`if(next_token()!=SYMBOL)`
`1095`	`1096`	`{`
`1096`	`1097`	`error() << "expected symbol in parameter" << eom;`
`1097`		`- return result;`
	`1098`	`+ return nil_typet();`
`1098`	`1099`	`}`
`1099`	`1100`
`1100`		`- auto &var=result.add_variable();`
	`1101`	`+ mathematical_function_typet::variablet var;`
`1101`	`1102`	`var.type()=sort();`
	`1103`	`+ domain.push_back(var);`
`1102`	`1104`
`1103`	`1105`	`if(next_token()!=CLOSE)`
`1104`	`1106`	`{`
`1105`	`1107`	`error() << "expected ')' at end of parameter" << eom;`
`1106`		`- return result;`
	`1108`	`+ return nil_typet();`
`1107`	`1109`	`}`
`1108`	`1110`	`}`
`1109`	`1111`
`1110`	`1112`	`next_token(); // eat the ')'`
`1111`	`1113`
`1112`		`- result.codomain()=sort();`
	`1114`	`+ typet codomain = sort();`
`1113`	`1115`
`1114`		`- return result;`
	`1116`	`+ return mathematical_function_typet(domain, codomain);`
`1115`	`1117`	`}`
`1116`	`1118`
`1117`	`1119`	`void smt2_parsert::command(const std::string &c)`