Add options structure to unit tests

Sonny Martin · Sonny Martin · commit ca1116608b2d · 2019-02-27T10:43:25.000Z
diff --git a/unit/goto-programs/goto_model_function_type_consistency.cpp b/unit/goto-programs/goto_model_function_type_consistency.cpp
@@ -11,6 +11,7 @@ Author: Diffblue Ltd.
 #include <util/arith_tools.h>
 
 #include <goto-programs/goto_model.h>
+#include <goto-programs/validate_goto_model.h>
 
 SCENARIO(
   "Validation of consistent program/table pair (function type)",
@@ -34,14 +35,16 @@ SCENARIO(
     goto_model.goto_functions.function_map[function_symbol.name].type =
       fun_type1;
 
+    goto_model_validation_optionst validation_options{false};
+
     WHEN("Symbol table has the right type")
     {
       function_symbol.type = fun_type1;
       goto_model.symbol_table.insert(function_symbol);
 
       THEN("The consistency check succeeds")
       {
-        goto_model.validate(validation_modet::INVARIANT);
+        goto_model.validate(validation_modet::INVARIANT, validation_options);
 
         REQUIRE(true);
       }
@@ -55,7 +58,7 @@ SCENARIO(
       THEN("The consistency check fails")
       {
         REQUIRE_THROWS_AS(
-          goto_model.validate(validation_modet::EXCEPTION),
+          goto_model.validate(validation_modet::EXCEPTION, validation_options),
           incorrect_goto_program_exceptiont);
       }
     }
diff --git a/unit/goto-programs/goto_program_assume.cpp b/unit/goto-programs/goto_program_assume.cpp
@@ -11,6 +11,7 @@ Author: Diffblue Ltd.
 #include <util/arith_tools.h>
 
 #include <goto-programs/goto_function.h>
+#include <goto-programs/validate_goto_model.h>
 
 SCENARIO(
   "Validation of well-formed assert/assume codes",
@@ -40,11 +41,14 @@ SCENARIO(
     namespacet ns(symbol_table);
     instructions.back() = goto_programt::make_assertion(x_le_10);
 
+    goto_model_validation_optionst validation_options;
+
     WHEN("Instruction has no targets")
     {
       THEN("The consistency check succeeds")
       {
-        goto_function.body.validate(ns, validation_modet::INVARIANT);
+        goto_function.body.validate(
+          ns, validation_modet::INVARIANT, validation_options);
         REQUIRE(true);
       }
     }
@@ -55,7 +59,7 @@ SCENARIO(
       THEN("The consistency check fails")
       {
         REQUIRE_THROWS_AS(
-          goto_function.body.validate(ns, validation_modet::EXCEPTION),
+          goto_function.body.validate(ns, validation_modet::EXCEPTION, validation_options),
           incorrect_goto_program_exceptiont);
       }
     }
diff --git a/unit/goto-programs/goto_program_dead.cpp b/unit/goto-programs/goto_program_dead.cpp
@@ -11,6 +11,7 @@ Author: Diffblue Ltd.
 #include <util/arith_tools.h>
 
 #include <goto-programs/goto_function.h>
+#include <goto-programs/validate_goto_model.h>
 
 SCENARIO(
   "Validation of well-formed symbol removing codes",
@@ -36,14 +37,17 @@ SCENARIO(
     instructions.emplace_back(goto_programt::make_dead(var_a));
     symbol_table.insert(fun_symbol);
 
+    goto_model_validation_optionst validation_options;
+
     WHEN("Removing known symbol")
     {
       symbol_table.insert(var_symbol);
       const namespacet ns(symbol_table);
 
       THEN("The consistency check succeeds")
       {
-        goto_function.body.validate(ns, validation_modet::INVARIANT);
+        goto_function.body.validate(
+          ns, validation_modet::INVARIANT, validation_options);
         REQUIRE(true);
       }
     }
@@ -55,7 +59,7 @@ SCENARIO(
       THEN("The consistency check fails")
       {
         REQUIRE_THROWS_AS(
-          goto_function.body.validate(ns, validation_modet::EXCEPTION),
+          goto_function.body.validate(ns, validation_modet::EXCEPTION, validation_options),
           incorrect_goto_program_exceptiont);
       }
     }
diff --git a/unit/goto-programs/goto_program_declaration.cpp b/unit/goto-programs/goto_program_declaration.cpp
@@ -9,6 +9,7 @@ Author: Diffblue Ltd.
 #include <testing-utils/use_catch.h>
 
 #include <goto-programs/goto_function.h>
+#include <goto-programs/validate_goto_model.h>
 
 #include <util/arith_tools.h>
 
@@ -36,14 +37,17 @@ SCENARIO(
     instructions.emplace_back(goto_programt::make_decl(var_a));
     symbol_table.insert(fun_symbol);
 
+    goto_model_validation_optionst validation_options;
+
     WHEN("Declaring known symbol")
     {
       symbol_table.insert(var_symbol);
       const namespacet ns(symbol_table);
 
       THEN("The consistency check succeeds")
       {
-        goto_function.body.validate(ns, validation_modet::INVARIANT);
+        goto_function.body.validate(
+          ns, validation_modet::INVARIANT, validation_options);
         REQUIRE(true);
       }
     }
@@ -55,7 +59,7 @@ SCENARIO(
       THEN("The consistency check fails")
       {
         REQUIRE_THROWS_AS(
-          goto_function.body.validate(ns, validation_modet::EXCEPTION),
+          goto_function.body.validate(ns, validation_modet::EXCEPTION, validation_options),
           incorrect_goto_program_exceptiont);
       }
     }
diff --git a/unit/goto-programs/goto_program_function_call.cpp b/unit/goto-programs/goto_program_function_call.cpp
@@ -11,6 +11,7 @@ Author: Diffblue Ltd.
 #include <util/arith_tools.h>
 
 #include <goto-programs/goto_function.h>
+#include <goto-programs/validate_goto_model.h>
 
 SCENARIO(
   "Validation of well-formed function call codes",
@@ -50,6 +51,8 @@ SCENARIO(
     symbol_table.insert(fun_symbol);
     namespacet ns(symbol_table);
 
+    goto_model_validation_optionst validation_options;
+
     WHEN("Return type matches")
     {
       code_function_callt function_call(var_a, fun_foo, {});
@@ -58,7 +61,8 @@ SCENARIO(
 
       THEN("The consistency check succeeds")
       {
-        goto_function.body.validate(ns, validation_modet::INVARIANT);
+        goto_function.body.validate(
+          ns, validation_modet::INVARIANT, validation_options);
         REQUIRE(true);
       }
     }
@@ -71,7 +75,7 @@ SCENARIO(
       THEN("The consistency check fails")
       {
         REQUIRE_THROWS_AS(
-          goto_function.body.validate(ns, validation_modet::EXCEPTION),
+          goto_function.body.validate(ns, validation_modet::EXCEPTION, validation_options),
           incorrect_goto_program_exceptiont);
       }
     }
diff --git a/unit/goto-programs/goto_program_goto_target.cpp b/unit/goto-programs/goto_program_goto_target.cpp
@@ -8,9 +8,10 @@ Author: Diffblue Ltd.
 
 #include <testing-utils/use_catch.h>
 
-#include <util/arith_tools.h>
-
 #include <goto-programs/goto_function.h>
+#include <goto-programs/validate_goto_model.h>
+
+#include <util/arith_tools.h>
 
 SCENARIO(
   "Validation of well-formed goto codes",
@@ -43,12 +44,15 @@ SCENARIO(
     symbol_table.insert(fun_symbol);
     namespacet ns(symbol_table);
 
+    goto_model_validation_optionst validation_options;
+
     WHEN("Target is a target")
     {
       instructions.front().target_number = 1;
       THEN("The consistency check succeeds")
       {
-        goto_function.body.validate(ns, validation_modet::INVARIANT);
+        goto_function.body.validate(
+          ns, validation_modet::INVARIANT, validation_options);
         REQUIRE(true);
       }
     }
@@ -58,7 +62,7 @@ SCENARIO(
       THEN("The consistency check fails")
       {
         REQUIRE_THROWS_AS(
-          goto_function.body.validate(ns, validation_modet::EXCEPTION),
+          goto_function.body.validate(ns, validation_modet::EXCEPTION, validation_options),
           incorrect_goto_program_exceptiont);
       }
     }
diff --git a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp
@@ -10,8 +10,9 @@ Author: Diffblue Ltd.
 
 #include <util/arith_tools.h>
 
-#include <goto-programs/goto_function.h>
-
+#include <goto-programs/goto_function.h>        
+#include <goto-programs/validate_goto_model.h>
+        
 SCENARIO(
   "Validation of consistent program/table pair (type-wise)",
   "[core][goto-programs][validate]")
@@ -36,6 +37,8 @@ SCENARIO(
     auto &instructions = goto_function.body.instructions;
     instructions.emplace_back(goto_programt::make_assertion(x_le_10));
 
+    goto_model_validation_optionst validation_options;
+
     symbol_table.insert(function_symbol);
     WHEN("Symbol table has the right symbol type")
     {
@@ -45,7 +48,8 @@ SCENARIO(
 
       THEN("The consistency check succeeds")
       {
-        goto_function.validate(ns, validation_modet::INVARIANT);
+        goto_function.validate(
+          ns, validation_modet::INVARIANT, validation_options);
 
         REQUIRE(true);
       }
@@ -60,7 +64,7 @@ SCENARIO(
       THEN("The consistency check fails")
       {
         REQUIRE_THROWS_AS(
-          goto_function.validate(ns, validation_modet::EXCEPTION),
+          goto_function.validate(ns, validation_modet::EXCEPTION, validation_options),
           incorrect_goto_program_exceptiont);
       }
     }
diff --git a/unit/goto-programs/goto_program_table_consistency.cpp b/unit/goto-programs/goto_program_table_consistency.cpp
@@ -11,6 +11,7 @@ Author: Diffblue Ltd.
 #include <util/arith_tools.h>
 
 #include <goto-programs/goto_function.h>
+#include <goto-programs/validate_goto_model.h>
 
 SCENARIO(
   "Validation of consistent program/table pair",
@@ -35,6 +36,8 @@ SCENARIO(
     auto &instructions = goto_function.body.instructions;
     instructions.emplace_back(goto_programt::make_assertion(x_le_10));
 
+    goto_model_validation_optionst validation_options;
+
     symbol_table.insert(function_symbol);
     WHEN("Symbol table has the right symbol")
     {
@@ -43,7 +46,8 @@ SCENARIO(
       const namespacet ns(symbol_table);
       THEN("The consistency check succeeds")
       {
-        goto_function.validate(ns, validation_modet::INVARIANT);
+        goto_function.validate(
+          ns, validation_modet::INVARIANT, validation_options);
         REQUIRE(true);
       }
     }
@@ -53,7 +57,7 @@ SCENARIO(
       THEN("The consistency check fails")
       {
         REQUIRE_THROWS_AS(
-          goto_function.validate(ns, validation_modet::EXCEPTION),
+          goto_function.validate(ns, validation_modet::EXCEPTION, validation_options),
           incorrect_goto_program_exceptiont);
       }
     }

Original file line number	Diff line number	Diff line change
`@@ -11,6 +11,7 @@ Author: Diffblue Ltd.`
`11`	`11`	`#include <util/arith_tools.h>`
`12`	`12`
`13`	`13`	`#include <goto-programs/goto_model.h>`
	`14`	`+#include <goto-programs/validate_goto_model.h>`
`14`	`15`
`15`	`16`	`SCENARIO(`
`16`	`17`	`"Validation of consistent program/table pair (function type)",`
`@@ -34,14 +35,16 @@ SCENARIO(`
`34`	`35`	`goto_model.goto_functions.function_map[function_symbol.name].type =`
`35`	`36`	`fun_type1;`
`36`	`37`
	`38`	`+ goto_model_validation_optionst validation_options{false};`
	`39`	`+`
`37`	`40`	`WHEN("Symbol table has the right type")`
`38`	`41`	`{`
`39`	`42`	`function_symbol.type = fun_type1;`
`40`	`43`	`goto_model.symbol_table.insert(function_symbol);`
`41`	`44`
`42`	`45`	`THEN("The consistency check succeeds")`
`43`	`46`	`{`
`44`		`- goto_model.validate(validation_modet::INVARIANT);`
	`47`	`+ goto_model.validate(validation_modet::INVARIANT, validation_options);`
`45`	`48`
`46`	`49`	`REQUIRE(true);`
`47`	`50`	`}`
`@@ -55,7 +58,7 @@ SCENARIO(`
`55`	`58`	`THEN("The consistency check fails")`
`56`	`59`	`{`
`57`	`60`	`REQUIRE_THROWS_AS(`
`58`		`- goto_model.validate(validation_modet::EXCEPTION),`
	`61`	`+ goto_model.validate(validation_modet::EXCEPTION, validation_options),`
`59`	`62`	`incorrect_goto_program_exceptiont);`
`60`	`63`	`}`
`61`	`64`	`}`
Original file line number	Diff line number	Diff line change
`@@ -9,6 +9,7 @@ Author: Diffblue Ltd.`
`9`	`9`	`#include <testing-utils/use_catch.h>`
`10`	`10`
`11`	`11`	`#include <goto-programs/goto_function.h>`
	`12`	`+#include <goto-programs/validate_goto_model.h>`
`12`	`13`
`13`	`14`	`#include <util/arith_tools.h>`
`14`	`15`
`@@ -36,14 +37,17 @@ SCENARIO(`
`36`	`37`	`instructions.emplace_back(goto_programt::make_decl(var_a));`
`37`	`38`	`symbol_table.insert(fun_symbol);`
`38`	`39`
	`40`	`+ goto_model_validation_optionst validation_options;`
	`41`	`+`
`39`	`42`	`WHEN("Declaring known symbol")`
`40`	`43`	`{`
`41`	`44`	`symbol_table.insert(var_symbol);`
`42`	`45`	`const namespacet ns(symbol_table);`
`43`	`46`
`44`	`47`	`THEN("The consistency check succeeds")`
`45`	`48`	`{`
`46`		`- goto_function.body.validate(ns, validation_modet::INVARIANT);`
	`49`	`+ goto_function.body.validate(`
	`50`	`+ ns, validation_modet::INVARIANT, validation_options);`
`47`	`51`	`REQUIRE(true);`
`48`	`52`	`}`
`49`	`53`	`}`
`@@ -55,7 +59,7 @@ SCENARIO(`
`55`	`59`	`THEN("The consistency check fails")`
`56`	`60`	`{`
`57`	`61`	`REQUIRE_THROWS_AS(`
`58`		`- goto_function.body.validate(ns, validation_modet::EXCEPTION),`
	`62`	`+ goto_function.body.validate(ns, validation_modet::EXCEPTION, validation_options),`
`59`	`63`	`incorrect_goto_program_exceptiont);`
`60`	`64`	`}`
`61`	`65`	`}`
Original file line number	Diff line number	Diff line change
`@@ -8,9 +8,10 @@ Author: Diffblue Ltd.`
`8`	`8`
`9`	`9`	`#include <testing-utils/use_catch.h>`
`10`	`10`
`11`		`-#include <util/arith_tools.h>`
`12`		`-`
`13`	`11`	`#include <goto-programs/goto_function.h>`
	`12`	`+#include <goto-programs/validate_goto_model.h>`
	`13`	`+`
	`14`	`+#include <util/arith_tools.h>`
`14`	`15`
`15`	`16`	`SCENARIO(`
`16`	`17`	`"Validation of well-formed goto codes",`
`@@ -43,12 +44,15 @@ SCENARIO(`
`43`	`44`	`symbol_table.insert(fun_symbol);`
`44`	`45`	`namespacet ns(symbol_table);`
`45`	`46`
	`47`	`+ goto_model_validation_optionst validation_options;`
	`48`	`+`
`46`	`49`	`WHEN("Target is a target")`
`47`	`50`	`{`
`48`	`51`	`instructions.front().target_number = 1;`
`49`	`52`	`THEN("The consistency check succeeds")`
`50`	`53`	`{`
`51`		`- goto_function.body.validate(ns, validation_modet::INVARIANT);`
	`54`	`+ goto_function.body.validate(`
	`55`	`+ ns, validation_modet::INVARIANT, validation_options);`
`52`	`56`	`REQUIRE(true);`
`53`	`57`	`}`
`54`	`58`	`}`
`@@ -58,7 +62,7 @@ SCENARIO(`
`58`	`62`	`THEN("The consistency check fails")`
`59`	`63`	`{`
`60`	`64`	`REQUIRE_THROWS_AS(`
`61`		`- goto_function.body.validate(ns, validation_modet::EXCEPTION),`
	`65`	`+ goto_function.body.validate(ns, validation_modet::EXCEPTION, validation_options),`
`62`	`66`	`incorrect_goto_program_exceptiont);`
`63`	`67`	`}`
`64`	`68`	`}`
Original file line number	Diff line number	Diff line change
`@@ -10,8 +10,9 @@ Author: Diffblue Ltd.`
`10`	`10`
`11`	`11`	`#include <util/arith_tools.h>`
`12`	`12`
`13`		`-#include <goto-programs/goto_function.h>`
`14`		`-`
	`13`	`+#include <goto-programs/goto_function.h>`
	`14`	`+#include <goto-programs/validate_goto_model.h>`
	`15`	`+`
`15`	`16`	`SCENARIO(`
`16`	`17`	`"Validation of consistent program/table pair (type-wise)",`
`17`	`18`	`"[core][goto-programs][validate]")`
`@@ -36,6 +37,8 @@ SCENARIO(`
`36`	`37`	`auto &instructions = goto_function.body.instructions;`
`37`	`38`	`instructions.emplace_back(goto_programt::make_assertion(x_le_10));`
`38`	`39`
	`40`	`+ goto_model_validation_optionst validation_options;`
	`41`	`+`
`39`	`42`	`symbol_table.insert(function_symbol);`
`40`	`43`	`WHEN("Symbol table has the right symbol type")`
`41`	`44`	`{`
`@@ -45,7 +48,8 @@ SCENARIO(`
`45`	`48`
`46`	`49`	`THEN("The consistency check succeeds")`
`47`	`50`	`{`
`48`		`- goto_function.validate(ns, validation_modet::INVARIANT);`
	`51`	`+ goto_function.validate(`
	`52`	`+ ns, validation_modet::INVARIANT, validation_options);`
`49`	`53`
`50`	`54`	`REQUIRE(true);`
`51`	`55`	`}`
`@@ -60,7 +64,7 @@ SCENARIO(`
`60`	`64`	`THEN("The consistency check fails")`
`61`	`65`	`{`
`62`	`66`	`REQUIRE_THROWS_AS(`
`63`		`- goto_function.validate(ns, validation_modet::EXCEPTION),`
	`67`	`+ goto_function.validate(ns, validation_modet::EXCEPTION, validation_options),`
`64`	`68`	`incorrect_goto_program_exceptiont);`
`65`	`69`	`}`
`66`	`70`	`}`