Document l2_thread_write_encoding

romainbrenguier · romainbrenguier · commit 6e5486b81e15 · 2019-06-17T08:47:22.000+01:00
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
@@ -514,6 +514,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
`@@ -514,6 +514,7 @@ goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared(`
`514`	`514`	`}`
`515`	`515`
`516`	`516`	`/// thread encoding`
	`517`	`+/// \return true if \p expr is shared between threads`
`517`	`518`	`bool goto_symex_statet::l2_thread_write_encoding(`
`518`	`519`	`const ssa_exprt &expr,`
`519`	`520`	`const namespacet &ns)`