Document l2_thread_write_encoding

romainbrenguier · romainbrenguier · commit 9f408f3a09cb · 2019-06-14T09:23:53.000+01:00
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
@@ -517,6 +517,7 @@ goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared(
 }
 
 /// thread encoding
+/// \return true if \p expr is shared between threads
 bool goto_symex_statet::l2_thread_write_encoding(
   const ssa_exprt &expr,
   const namespacet &ns)

Original file line number	Diff line number	Diff line change
`@@ -517,6 +517,7 @@ goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared(`
`517`	`517`	`}`
`518`	`518`
`519`	`519`	`/// thread encoding`
	`520`	`+/// \return true if \p expr is shared between threads`
`520`	`521`	`bool goto_symex_statet::l2_thread_write_encoding(`
`521`	`522`	`const ssa_exprt &expr,`
`522`	`523`	`const namespacet &ns)`