Work around test diff by hiding CE

CHANGELOG.md

@@ -27,7 +27,9 @@ generated in the following situations:
 
 ### 1.1.9-dev
 
-
+* [TRLC] Add new option `--no-detailed-info` which supresses the
+  additional information the linter may add to a message, such as
+  counter-examples or reasoning.
 
 ### 1.1.8
 

tests-system/Makefile

@@ -14,19 +14,23 @@ all: $(TARGETS) bulk/output bulk/output.brief bulk/output.lint bulk/output.json
 %/output:
 	-@coverage run -p --rcfile=../coverage.cfg --branch \
 		--data-file ../.coverage \
-		../trlc.py $(dir $@) > $@
+		../trlc.py $(file < $(dir $@)options) \
+			$(dir $@) > $@
 
 %/output.brief:
 	-@coverage run -p --rcfile=../coverage.cfg --branch \
 		--data-file ../.coverage \
-		../trlc.py --brief $(dir $@) > $@
+		../trlc.py $(file < $(dir $@)options) \
+			--brief $(dir $@) > $@
 
 %/output.lint:
 	-@coverage run -p --rcfile=../coverage.cfg --branch \
 		--data-file ../.coverage \
-		../trlc.py --lint --verify $(dir $@) > $@
+		../trlc.py $(file < $(dir $@)options) \
+			--lint --verify $(dir $@) > $@
 
 %/output.json:
 	-@coverage run -p --rcfile=../coverage.cfg --branch \
 		--data-file ../.coverage \
-		../trlc.py --debug-api-dump $(dir $@) > $@
+		../trlc.py $(file < $(dir $@)options) \
+			--debug-api-dump $(dir $@) > $@

tests-system/lint-vcg-strings/options

@@ -0,0 +1 @@
+--no-detailed-info

tests-system/lint-vcg-strings/output.lint

@@ -1,24 +1,7 @@
 y, "potato"
 ^ lint-vcg-strings/test1.rsl:15: warning: expression could be null [vcg-evaluation-of-null]
-| example record_type triggering error:
-|   T bad_potato {
-|     x = "mBCDkitten?"
-|     /* y is null */
-|   }
 c, "potato"
 ^ lint-vcg-strings/test2.rsl:14: warning: expression could be null [vcg-evaluation-of-null]
-| example record_type triggering error:
-|   T bad_potato {
-|     x = "foo"
-|     y = "AAAAbar"
-|     /* c is null */
-|   }
 c,              warning "potato"
 ^ lint-vcg-strings/test3.rsl:11: warning: expression could be null [vcg-evaluation-of-null]
-| example record_type triggering error:
-|   T bad_potato {
-|     s = '''pot
-| ato'''
-|     /* c is null */
-|   }
 Verified 3 model(s) and 0 check(s) and found 3 warning(s)

trlc/errors.py

@@ -123,9 +123,10 @@ class Message_Handler:
     :type: int
 
     """
-    def __init__(self, brief=False):
+    def __init__(self, brief=False, detailed_info=True):
         assert isinstance(brief, bool)
         self.brief             = brief
+        self.show_details      = detailed_info
         self.warnings          = 0
         self.errors            = 0
         self.suppressed        = 0
@@ -174,7 +175,9 @@ def emit(self, location, kind, message, fatal=True, extrainfo=None):
             else:
                 print(msg)
 
-            if not self.brief and extrainfo:
+            if not self.brief \
+               and self.show_details \
+               and extrainfo:
                 if context:
                     indent = len(context[1]) - 1
                 else:

trlc/trlc.py

@@ -421,11 +421,20 @@ def main():
     og_linter.add_argument("--verify",
                            default=False,
                            action="store_true",
-                           help=("[EXPERIMENTAL] Attempt to statically "
+                           help=("[EXPERIMENTAL] Attempt to statically"
                                  " verify absence of errors in user defined"
                                  " checks. Does not yet support all language"
                                  " constructs. Requires PyVCG to be "
                                  " installed."))
+    og_linter.add_argument("--no-detailed-info",
+                           default=False,
+                           action="store_true",
+                           help=("Do not print counter-examples and other"
+                                 " supplemental information on failed"
+                                 " checks. The specific values of"
+                                 " counter-examples are unpredictable"
+                                 " from system to system, so if you need 100%"
+                                 " reproducible output then use this option."))
 
     og_debug = ap.add_argument_group("debug options")
     og_debug.add_argument("--debug-dump",
@@ -451,7 +460,7 @@ def main():
     if options.verify and not VCG_AVAILABLE:
         ap.error("The --verify option requires the optional dependency PyVCG")
 
-    mh = Message_Handler(options.brief)
+    mh = Message_Handler(options.brief, not options.no_detailed_info)
 
     if options.no_user_warnings:
         mh.suppress("check warning")