Add regression tests for invalid usage of --nondet-volatile-model

Author: danpoe

regression/goto-instrument/nondet-volatile-model-04/test.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+volatile int a;
+
+float model()
+{
+  return 1;
+}
+
+void main()
+{
+  a;
+}

regression/goto-instrument/nondet-volatile-model-04/test1.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--nondet-volatile-model a:model
+^Invalid User Input$
+return type of model .* is not compatible with the type of the modelled variable
+^EXIT=1$
+^SIGNAL=0$
+--
+--
+Check that the command line typechecking reports when a model with a return type
+that is incompatible with the type of the modelled variable is given

regression/goto-instrument/nondet-volatile-model-04/test2.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--nondet-volatile-model a:non_existing_model
+^Invalid User Input$
+given model name .* not found in symbol table
+^EXIT=1$
+^SIGNAL=0$
+--
+--
+Check that the command line typechecking reports when a given model for a
+variable cannot be found

regression/goto-instrument/nondet-volatile-model-05/test.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+volatile int a;
+
+int model_a()
+{
+  return 1;
+}
+
+int model_b()
+{
+  return 2;
+}
+
+void main()
+{
+  a;
+}

regression/goto-instrument/nondet-volatile-model-05/test1.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--nondet-volatile-model a:model_a --nondet-volatile-model a:model_b
+^Invalid User Input$
+conflicting models for variable
+^EXIT=1$
+^SIGNAL=0$
+--
+--
+Check that the command line typechecking reports when two conflicting models are
+given for a variable

regression/goto-instrument/nondet-volatile-model-05/test2.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--nondet-volatile-model a:model_a --nondet-volatile-variable a
+^Invalid User Input$
+conflicting options for variable
+^EXIT=1$
+^SIGNAL=0$
+--
+--
+Check that the command line typechecking reports when conflicting options are
+given for a variable