goto-analyzer: Use capitals when outputting results

This is to match what the other tools (CBMC, symex, etc.) do.

Author: Daniel Kroening

regression/goto-analyzer/constant_propagation_05/test.desc

@@ -3,6 +3,6 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 12 function main, assertion j != 3: Failure \(if reachable\)$
+^\[main.assertion.1\] file main.c line 12 function main, assertion j != 3: FAILURE \(if reachable\)$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_06/test.desc

@@ -3,6 +3,6 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 11 function main, assertion i\s*<\s*51: Unknown$
+^\[main.assertion.1\] file main.c line 11 function main, assertion i\s*<\s*51: UNKNOWN$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_10/test.desc

@@ -3,6 +3,6 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 10 function main, assertion a\[(\(signed( long)? long int\))?0\] == 2: Failure$
+^\[main.assertion.1\] file main.c line 10 function main, assertion a\[(\(signed( long)? long int\))?0\] == 2: FAILURE$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_13/test.desc

@@ -3,6 +3,6 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 9 function main, assertion y == 0: Failure \(if reachable\)$
+^\[main.assertion.1\] file main.c line 9 function main, assertion y == 0: FAILURE \(if reachable\)$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_14/test.desc

@@ -3,7 +3,7 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 11 function main, assertion tmp_if_expr: Success$
-^\[main.assertion.2\] file main.c line 12 function main, assertion tmp_if_expr\$1: Failure$
+^\[main.assertion.1\] file main.c line 11 function main, assertion tmp_if_expr: SUCCESS$
+^\[main.assertion.2\] file main.c line 12 function main, assertion tmp_if_expr\$1: FAILURE$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_15/test.desc

@@ -3,6 +3,6 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 9 function main, assertion a\[(\(signed( long)? long int\))?0\] == 2: Failure$
+^\[main.assertion.1\] file main.c line 9 function main, assertion a\[(\(signed( long)? long int\))?0\] == 2: FAILURE$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_17/test.desc

@@ -3,6 +3,6 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 12 function main, assertion i\s*<\s*51: (Unknown|Failure \(if reachable\))$
+^\[main.assertion.1\] file main.c line 12 function main, assertion i\s*<\s*51: (UNKNOWN|FAILURE \(if reachable\))$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_floating_point_div/test.desc

@@ -3,6 +3,6 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 8 function main, assertion eight == 8: Success$
+^\[main.assertion.1\] file main.c line 8 function main, assertion eight == 8: SUCCESS$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc

@@ -3,11 +3,11 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-\[main.assertion.1\] file main.c line 18 function main, assertion \(1.0f / 10.0f\) - f < -0.1f: Failure \(if reachable\)
-\[main.assertion.2\] file main.c line 20 function main, assertion \(1.0f / 10.0f\) - f < 0.0f: Unknown
-\[main.assertion.3\] file main.c line 22 function main, assertion \(1.0f / 10.0f\) - f <= 0.0f: Success
-\[main.assertion.4\] file main.c line 24 function main, assertion \(1.0f / 10.0f\) - f >= 0.0f: Unknown
-\[main.assertion.5\] file main.c line 26 function main, assertion \(1.0f / 10.0f\) - f > 0.0f: Failure \(if reachable\)
+\[main.assertion.1\] file main.c line 18 function main, assertion \(1.0f / 10.0f\) - f < -0.1f: FAILURE \(if reachable\)
+\[main.assertion.2\] file main.c line 20 function main, assertion \(1.0f / 10.0f\) - f < 0.0f: UNKNOWN
+\[main.assertion.3\] file main.c line 22 function main, assertion \(1.0f / 10.0f\) - f <= 0.0f: SUCCESS
+\[main.assertion.4\] file main.c line 24 function main, assertion \(1.0f / 10.0f\) - f >= 0.0f: UNKNOWN
+\[main.assertion.5\] file main.c line 26 function main, assertion \(1.0f / 10.0f\) - f > 0.0f: FAILURE \(if reachable\)
 
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_rounding_mode/test.desc

@@ -3,7 +3,7 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 9 function main, assertion rounded_up - 0.1f >= 0: Success
-^\[main.assertion.2\] file main.c line 10 function main, assertion rounded_down - 0.1f < 0: Success
+^\[main.assertion.1\] file main.c line 9 function main, assertion rounded_up - 0.1f >= 0: SUCCESS
+^\[main.assertion.2\] file main.c line 10 function main, assertion rounded_down - 0.1f < 0: SUCCESS
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_01/test.desc

@@ -3,13 +3,13 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 7 function main, assertion i\s*>=\s*10: Success$
-^\[main.assertion.2\] file main.c line 10 function main, assertion i\s*!=\s*30: Success$
-^\[main.assertion.3\] file main.c line 13 function main, assertion i\s*!=\s*15: Unknown$
-^\[main.assertion.4\] file main.c line 16 function main, assertion 0: Success$
-^\[main.assertion.5\] file main.c line 19 function main, assertion j\s*>=\s*10: Success$
-^\[main.assertion.6\] file main.c line 22 function main, assertion i\s*>=\s*j: Unknown$
-^\[main.assertion.7\] file main.c line 25 function main, assertion i\s*>=\s*11: Success$
-^\[main.assertion.8]\ file main.c line 28 function main, assertion j\s*<\s*100: Success$
+^\[main.assertion.1\] file main.c line 7 function main, assertion i\s*>=\s*10: SUCCESS$
+^\[main.assertion.2\] file main.c line 10 function main, assertion i\s*!=\s*30: SUCCESS$
+^\[main.assertion.3\] file main.c line 13 function main, assertion i\s*!=\s*15: UNKNOWN$
+^\[main.assertion.4\] file main.c line 16 function main, assertion 0: SUCCESS$
+^\[main.assertion.5\] file main.c line 19 function main, assertion j\s*>=\s*10: SUCCESS$
+^\[main.assertion.6\] file main.c line 22 function main, assertion i\s*>=\s*j: UNKNOWN$
+^\[main.assertion.7\] file main.c line 25 function main, assertion i\s*>=\s*11: SUCCESS$
+^\[main.assertion.8]\ file main.c line 28 function main, assertion j\s*<\s*100: SUCCESS$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_02/test.desc

@@ -3,6 +3,6 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 5 function main, assertion x > -10 \&\& x < 100: Success$
+^\[main.assertion.1\] file main.c line 5 function main, assertion x > -10 \&\& x < 100: SUCCESS$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_03/test.desc

@@ -3,6 +3,6 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 6 function main, assertion x > -10 \|\| x < 100: Success$
+^\[main.assertion.1\] file main.c line 6 function main, assertion x > -10 \|\| x < 100: SUCCESS$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_04/test.desc

@@ -3,6 +3,6 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 8 function main, assertion i >= 1 && i <= 2: Success$
+^\[main.assertion.1\] file main.c line 8 function main, assertion i >= 1 && i <= 2: SUCCESS$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_05/test.desc

@@ -3,6 +3,6 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 8 function main, assertion i >= 1 \|\| i <= 2: Success$
+^\[main.assertion.1\] file main.c line 8 function main, assertion i >= 1 \|\| i <= 2: SUCCESS$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_06/test.desc

@@ -3,6 +3,6 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 \|\| x > 100: Failure \(if reachable\)$
+^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 \|\| x > 100: FAILURE \(if reachable\)$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_07/test.desc

@@ -3,6 +3,6 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 \&\& x > 100: Failure \(if reachable\)$
+^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 \&\& x > 100: FAILURE \(if reachable\)$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_08/test.desc

@@ -3,6 +3,6 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 6 function main, assertion x < -10 \&\& x < 100: Failure \(if reachable\)$
+^\[main.assertion.1\] file main.c line 6 function main, assertion x < -10 \&\& x < 100: FAILURE \(if reachable\)$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_09/test.desc

@@ -3,6 +3,6 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 8 function main, assertion i >= 1 \&\& i <= 2: Success$
+^\[main.assertion.1\] file main.c line 8 function main, assertion i >= 1 \&\& i <= 2: SUCCESS$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_10/test.desc

@@ -5,8 +5,8 @@ main.c
 ^SIGNAL=0$
 ^\[main.assertion.1\] file main.c line 8 function main, assertion j<=100: Success$
 ^\[main.assertion.2\] file main.c line 11 function main, assertion j<101: Success$
-^\[main.assertion.3\] file main.c line 14 function main, assertion j>100: Failure \(if reachable\)$
-^\[main.assertion.4\] file main.c line 17 function main, assertion j<99: Unknown$
-^\[main.assertion.5\] file main.c line 20 function main, assertion j==100: Failure \(if reachable\)$
+^\[main.assertion.3\] file main.c line 14 function main, assertion j>100: FAILURE \(if reachable\)$
+^\[main.assertion.4\] file main.c line 17 function main, assertion j<99: UNKNOWN$
+^\[main.assertion.5\] file main.c line 20 function main, assertion j==100: FAILURE \(if reachable\)$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_11/test.desc

@@ -3,7 +3,7 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 30 function main, assertion y\[i\]>=-1.0f \&\& y\[i\]<=1.0f: Unknown$
-^\[main.assertion.2\] file main.c line 35 function main, assertion y\[i\]>=-1.0f \&\& y\[i\]<=1.0f: Unknown$
+^\[main.assertion.1\] file main.c line 30 function main, assertion y\[i\]>=-1.0f \&\& y\[i\]<=1.0f: UNKNOWN$
+^\[main.assertion.2\] file main.c line 35 function main, assertion y\[i\]>=-1.0f \&\& y\[i\]<=1.0f: UNKNOWN$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_12/test.desc

@@ -3,7 +3,7 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^[main.assertion.1] file main.c line 8 function main, assertion j < 0: Success$
-^[main.assertion.2] file main.c line 11 function main, assertion j < 0: Success$
+^[main.assertion.1] file main.c line 8 function main, assertion j < 0: SUCCESS$
+^[main.assertion.2] file main.c line 11 function main, assertion j < 0: SUCCESS$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_13/test.desc

@@ -3,13 +3,13 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 7 function main, assertion i\s*>=\s*10: Success$
-^\[main.assertion.2\] file main.c line 10 function main, assertion i\s*!=\s*30: Success$
-^\[main.assertion.3\] file main.c line 13 function main, assertion i\s*!=\s*15: Unknown$
-^\[main.assertion.4\] file main.c line 16 function main, assertion 0: Success$
-^\[main.assertion.5\] file main.c line 19 function main, assertion j\s*>=\s*10: Success$
-^\[main.assertion.6\] file main.c line 22 function main, assertion i\s*>=\s*j: Unknown$
-^\[main.assertion.7\] file main.c line 25 function main, assertion i\s*>=\s*11: Success$
-^\[main.assertion.8\] file main.c line 28 function main, assertion j\s*<\s*100: Success$
+^\[main.assertion.1\] file main.c line 7 function main, assertion i\s*>=\s*10: SUCCESS$
+^\[main.assertion.2\] file main.c line 10 function main, assertion i\s*!=\s*30: SUCCESS$
+^\[main.assertion.3\] file main.c line 13 function main, assertion i\s*!=\s*15: UNKNOWN$
+^\[main.assertion.4\] file main.c line 16 function main, assertion 0: SUCCESS$
+^\[main.assertion.5\] file main.c line 19 function main, assertion j\s*>=\s*10: SUCCESS$
+^\[main.assertion.6\] file main.c line 22 function main, assertion i\s*>=\s*j: UNKNOWN$
+^\[main.assertion.7\] file main.c line 25 function main, assertion i\s*>=\s*11: SUCCESS$
+^\[main.assertion.8\] file main.c line 28 function main, assertion j\s*<\s*100: SUCCESS$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_14/test.desc

@@ -3,8 +3,8 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 12 function main, assertion i<50: Unknown$
-^\[main.assertion.2\] file main.c line 13 function main, assertion i<51: Unknown$
-^\[main.assertion.3\] file main.c line 14 function main, assertion i<52: Success$
+^\[main.assertion.1\] file main.c line 12 function main, assertion i<50: UNKNOWN$
+^\[main.assertion.2\] file main.c line 13 function main, assertion i<51: UNKNOWN$
+^\[main.assertion.3\] file main.c line 14 function main, assertion i<52: SUCCESS$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_15/test.desc

@@ -3,6 +3,6 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 11 function main, assertion j\s*<\s*52: Unknown$
+^\[main.assertion.1\] file main.c line 11 function main, assertion j\s*<\s*52: UNKNOWN$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_16/test.desc

@@ -3,6 +3,6 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 11 function main, assertion j\s*<\s*52: (Unknown|Failure \(if reachable\))$
+^\[main.assertion.1\] file main.c line 11 function main, assertion j\s*<\s*52: (UNKNOWN|FAILURE \(if reachable\))$
 --
 ^warning: ignoring

regression/goto-analyzer/sensitivity-function-call-recursive/test.desc

@@ -3,9 +3,9 @@ main.c
 --variable --pointers --arrays --structs --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.assertion\.1\] .* assertion y==4: Unknown$
-^\[main\.assertion\.2\] .* assertion y2==0: Unknown$
-^\[main\.assertion\.3\] .* assertion z==0: Success$
-^\[main\.assertion\.4\] .* assertion w==18: Success$
+^\[main\.assertion\.1\] .* assertion y==4: UNKNOWN$
+^\[main\.assertion\.2\] .* assertion y2==0: UNKNOWN$
+^\[main\.assertion\.3\] .* assertion z==0: SUCCESS$
+^\[main\.assertion\.4\] .* assertion w==18: SUCCESS$
 --
 ^warning: ignoring