Remove obsolete declaration and make functions static for --nondet-volatile feature

danpoe · danpoe · commit ff4a7b60aa40 · 2020-05-27T17:26:41.000+01:00
diff --git a/src/goto-instrument/nondet_volatile.cpp b/src/goto-instrument/nondet_volatile.cpp
@@ -31,7 +31,7 @@ static bool is_volatile(const namespacet &ns, const typet &src)
   return false;
 }
 
-void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
+static void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
 {
   Forall_operands(it, expr)
     nondet_volatile_rhs(symbol_table, *it);
@@ -52,7 +52,7 @@ void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
   }
 }
 
-void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
+static void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
 {
   if(expr.id()==ID_if)
   {
@@ -75,9 +75,8 @@ void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
   }
 }
 
-void nondet_volatile(
-  symbol_tablet &symbol_table,
-  goto_programt &goto_program)
+static void
+nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
 {
   namespacet ns(symbol_table);
 
diff --git a/src/goto-instrument/nondet_volatile.h b/src/goto-instrument/nondet_volatile.h
@@ -14,10 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/goto_model.h>
 
-bool is_volatile(
-  const symbol_tablet &,
-  const typet &);
-
 void nondet_volatile(goto_modelt &);
 
 #endif // CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H

Original file line number	Diff line number	Diff line change
`@@ -31,7 +31,7 @@ static bool is_volatile(const namespacet &ns, const typet &src)`
`31`	`31`	`return false;`
`32`	`32`	`}`
`33`	`33`
`34`		`-void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)`
	`34`	`+static void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)`
`35`	`35`	`{`
`36`	`36`	`Forall_operands(it, expr)`
`37`	`37`	`nondet_volatile_rhs(symbol_table, *it);`
`@@ -52,7 +52,7 @@ void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)`
`52`	`52`	`}`
`53`	`53`	`}`
`54`	`54`
`55`		`-void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)`
	`55`	`+static void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)`
`56`	`56`	`{`
`57`	`57`	`if(expr.id()==ID_if)`
`58`	`58`	`{`
`@@ -75,9 +75,8 @@ void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)`
`75`	`75`	`}`
`76`	`76`	`}`
`77`	`77`
`78`		`-void nondet_volatile(`
`79`		`- symbol_tablet &symbol_table,`
`80`		`- goto_programt &goto_program)`
	`78`	`+static void`
	`79`	`+nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)`
`81`	`80`	`{`
`82`	`81`	`namespacet ns(symbol_table);`
`83`	`82`