Merge pull request #7163 from thomasspriggs/tas/goto-analyzer-warning

thomasspriggs · web-flow · commit cf00a53bbcc3 · 2022-10-05T14:18:18.000+01:00
Add warning about unsound simplification in goto-analyzer
diff --git a/regression/goto-analyzer-simplify/soundness-warning/main.c b/regression/goto-analyzer-simplify/soundness-warning/main.c
@@ -0,0 +1,4 @@
+
+void main()
+{
+}
diff --git a/regression/goto-analyzer-simplify/soundness-warning/test.desc b/regression/goto-analyzer-simplify/soundness-warning/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--vsd --vsd-values constants
+\*\*\*\* WARNING\: This simplification is currently known to be unsound for input programs which include recursion\. Do not use it if soundness is important for your use case\.
+^SIGNAL=0$
+^EXIT=0$
+--
diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
@@ -56,6 +56,10 @@ bool static_simplifier(
 
   messaget m(message_handler);
   m.status() << "Simplifying program" << messaget::eom;
+  m.warning() << "**** WARNING: This simplification is currently known to be "
+                 "unsound for input programs which include recursion. Do not "
+                 "use it if soundness is important for your use case."
+              << messaget::eom;
 
   for(auto &gf_entry : goto_model.goto_functions.function_map)
   {

-Original file line number
+Diff line change
@@ @@ -0,0 +1,4 @@ @@
++
 +void main()
 +{
 +}
Original file line number	Diff line number	Diff line change
`@@ -56,6 +56,10 @@ bool static_simplifier(`
`56`	`56`
`57`	`57`	`messaget m(message_handler);`
`58`	`58`	`m.status() << "Simplifying program" << messaget::eom;`
	`59`	`+ m.warning() << "**** WARNING: This simplification is currently known to be "`
	`60`	`+ "unsound for input programs which include recursion. Do not "`
	`61`	`+ "use it if soundness is important for your use case."`
	`62`	`+ << messaget::eom;`
`59`	`63`
`60`	`64`	`for(auto &gf_entry : goto_model.goto_functions.function_map)`
`61`	`65`	`{`